Observation-level-driven formal modeling

Autoren Atif Mashkoor
J.-P. Jacquot
Titel Observation-level-driven formal modeling
Buchtitel Proceedings of the 16th IEEE International Symposium on High Assurance Systems Engineering (HASE 2015)
Typ in Konferenzband
Verlag IEEE
ISBN 978-1-4799-8110-6
DOI 10.1109/HASE.2015.32
Monat January
Jahr 2015
Seiten 158-165
SCCH ID# 1461

Refinement-based formal methods provide a systematic process to develop software that is correct by construction through a gradual enrichment of models. However, their waterfall-like linear sequence of refinements makes it difficult to express properties at the desired level of abstraction without cluttering the models' specification. Consequently, models become difficult to develop, organize and understand. In this paper, we present an approach based on the notion of "observation levels" to organize the model development in such a way that facilitates the inclusion of new properties into the model without compromising its understand ability. The approach is demonstrated by its application on two real-life high-assurance case studies.