A Specification Patterns System for Discrete Event Systems Analysis. (27th August 2013)

• Record Type: Journal Article
• Authors: Campos, Jose Creissac; Machado, Jose
• Is Part Of: International journal of advanced robotic systems. Volume 10:Number 8(2013)
• Publication Date: 2013-08-27
• Subjects: Discrete Event Systems -- Dependability -- Model Checking -- Property Specification Patterns; Robotics -- Periodicals; Robotics; Periodicals; 629.892
• DOI: 10.5772/56412
• Languages: English
• ISSNs: 1729-8806

Abstract

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.