J. C. Campos, J. Machado and E. Seabra
Property Patterns for the Formal Verification of Automated Production Systems
In Proceedings of the 17th IFAC World Congress, pages 5107-5112. IFAC. 2008.
Abstract

In recent years, several approaches to the analysis of automation systems dependability through the application of formal verification techniques have been proposed. Much of the research has been concerned with the modelling languages used, and how best to express the automation systems, so that automated veri cation might be possible. Less attention, however, has been devoted to the process of writing properties that accurately capture the requirements that need veri cation. This is however a crucial aspect of the veri cation process. Writing appropriate properties, in a logic suitable for veri cation, is a skilful process, and indeed there have been reports of properties being wrongly expressed. In this paper we put forward a tool and a collection of property patterns that aim at providing help in this area.

download PDF 

@InProceedings{CamposMS:2008,
 author = {J. C. Campos and J. Machado and E. Seabra},
 title = {Property Patterns for the Formal Verification of Automated Production Systems},
 booktitle = {Proceedings of the 17th IFAC World Congress},
 pages = {5107-5112},
 year = {2008},
 publisher = {IFAC},
 paperurl = {http://www.nt.ntnu.no/users/skoge/prost/proceedings/ifac2008/data/papers/4192.pdf},
 abstract = {In recent years, several approaches to the analysis of automation systems dependability through the application of formal verification techniques have been proposed. Much of the research has been concerned with the modelling languages used, and how best to express the automation systems, so that automated verication might be possible. Less attention, however, has been devoted to the process of writing properties that accurately capture the requirements that need verication. This is however a crucial aspect of the verication process. Writing appropriate properties, in a logic suitable for verication, is a skilful process, and indeed there have been reports of properties being wrongly expressed. In this paper we put forward a tool and a collection of property patterns that aim at providing help in this area.}
}

Generated by mkBiblio 2.6.26