Observation-Level-Driven Formal Modeling

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.