Observation-level-driven formal modeling

Autoren Atif Mashkoor
J.-P. Jacquot
Editoren
TitelObservation-level-driven formal modeling
BuchtitelProceedings of the 16th IEEE International Symposium on High Assurance Systems Engineering (HASE 2015)
Typin Konferenzband
VerlagIEEE
ISBN978-1-4799-8110-6
DOI10.1109/HASE.2015.32
MonatJanuary
Jahr2015
Seiten158-165
SCCH ID#1461
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.