OpenAIRE is about to release its new face with lots of new content and services.
During September, you may notice downtime in services, while some functionalities (e.g. user registration, login, validation, claiming) will be temporarily disabled.
We apologize for the inconvenience, please stay tuned!
For further information please contact helpdesk[at]

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

Cookies make it easier for us to provide you with our services. With the usage of our services you permit us to use cookies.
More information Ok