Modal logic as a design notation
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...
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | CONF |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_08186843_v_n_p150_Areces |
| Aporte de: |
| Sumario: | 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. |
|---|