Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Mencák, Jirí
Languages: English
Types: Doctoral thesis
Subjects: QA75
Formal methods are gaining popularity as a way of increasing the reliability of systems through\ud the use of mathematically based techniques. Their domain is no longer restricted to purely\ud academic environments and examples, as they are slowly moving into industrial settings. The\ud slow rate at which this transition takes place is mainly due to the perceived difficulty of\ud formalising the behaviour of systems. While this is undoubtedly true, it is not the case with\ud all formal methods.\ud \ud \ud Update Plans are a powerful formalism for the description of computer architectures\ud and intermediate to low-level languages. They are a declarative specification language with\ud an underlying imperative machine model. The descriptions using Update Plans are clear,\ud compact, intuitive, unambiguous and simple to read. These characteristics allow for the\ud minimisation of possible errors at early stages of the development process even before a\ud verification takes place.\ud \ud \ud In this thesis an overview of the Update Plans formalism is given and a number of realworld\ud applications is shown. The investigation of the application area focuses on computer\ud architectures for which various specifications already exist. The comparison of Update Plan\ud specifications to other specifications provides a useful insight into the strengths and shortcomings\ud of the formalism. The shortcomings, in particular the lack of synchronisation primitives\ud and modularity, are addressed by the development and evaluation of several syntactic and\ud semantic extensions described in this thesis. The extended formalism is also compared to\ud other specification languages and conclusions are drawn.
  • No references.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article