期刊名称：International Journal of Advanced Robotic Systems
印刷版ISSN：1729-8806
电子版ISSN：1729-8814
出版年度：2013
卷号：10
期号：8
页码：315
DOI：10.5772/56412
语种：English
出版社：SAGE Publications
摘要：As formal verification tools gain popularity, the problem arises of making them more accessible to engineers. A correct understanding of the logics used to express the properties of a system's behaviour is needed in order to guarantee that properties correctly encode the intent of the verification process. Writing appropriate properties, in a logic suitable for verification, is a skilful process. Errors in this step of the process can create serious problems since a false sense of safety is gained from the analysis. However, when compared to the effort put into developing and applying modelling languages, little attention has been devoted to the process of writing properties that accurately capture verification requirements. In this paper we illustrate how a collection of property patterns can help in simplifying the process of generating logical formulae from informally expressed requirements.
关键词：Discrete Event Systems; Dependability; Model Checking; Property Specification Patterns
Loading...
