Modal logic as a design notation
Carlos Areces, Miguel Felder, Dan Hirsch, Daniel Yankelevich · 1998
A notation to describe software system designs is given together with the means to verify properties over them. Designs are considered as models of a modal logic. The procedure to derive the modal model associated to a design, the algorithm to check properties over a model, the method to define new relations and the method of model filtration are presented. The proposed logic (KPI a poly-modal logic with inverse operators) is used as a property specification language verified through a model checking algorithm. The methods provided proved to be effective and simple to implement. A prototype tool has been developed in SML-NJ covering all functionalities described. 1 Introduction The successful development of software systems requires adequate tools. These tools have to be at the same time powerful, simple and formal. There are different tools for the different steps of the Software Development Cycle. In our work, we will devote special attention to the Design Step. Structured Design ...