Observation-level-driven formal modeling

A. Mashkoor, J. Jacquot. Observation-level-driven formal modeling. pages 158-165, DOI 10.1109/HASE.2015.32, 1, 2015.

Autoren
  • Atif Mashkoor
  • J.-P. Jacquot
BuchProceedings of the 16th IEEE International Symposium on High Assurance Systems Engineering (HASE 2015)
TypIn Konferenzband
VerlagIEEE
DOI10.1109/HASE.2015.32
ISBN978-1-4799-8110-6
Monat1
Jahr2015
Seiten158-165
Abstract

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.