Observation-level-driven formal modeling

Authors Atif Mashkoor
J.-P. Jacquot
Title Observation-level-driven formal modeling
Booktitle Proceedings of the 16th IEEE International Symposium on High Assurance Systems Engineering (HASE 2015)
Type in proceedings
Publisher IEEE
ISBN 978-1-4799-8110-6
DOI 10.1109/HASE.2015.32
Month January
Year 2015
Pages 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.