Observation-Level-Driven Formal Modeling

International audienceRefinement-based formal methods provide a sys- tematic process to develop software that is correct by construc- tion 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 compro- mising its understandability. The approach is demonstrated by its application on two real-life high-assurance case studies