Modal Logic as a Design Notation (position paper)

C. Areces, M. Felder, D. Hirsch, and D. Yankelevich. Modal Logic as a Design Notation (position paper). In Proceedings of the 9th International Workshop on Software Specification and Design (IWSSD9), pp. 150–152, Ise-Shima, Japan, 1998.

Download

[pdf] 

Abstract

A notation to describe software system designs is given together with the means to verify properties over them. De- signs are considered as models of a modal logic. The pro- cedure to derive the modal model associated to a design, the algorithm to check properties over a model, the method to de ne new relations and the method of model ltration are presented. The proposed logic (KPI a poly-modal logic with inverse operators) is used as a property speci cation language veri ed through a model checking algorithm. The methods provided proved to be e ective and simple to im- plement. A prototype tool has been developed in SML-NJ covering all functionalities described.

BibTeX

@InCollection{Areces1998b,
  author =       "C. Areces and M. Felder and D. Hirsch and D.
                 Yankelevich",
  booktitle =    "Proceedings of the 9th International Workshop on
                 Software Specification and Design (IWSSD9)",
  title =        "Modal Logic as a Design Notation (position paper)",
  year =         "1998",
  address =      "Ise-Shima, Japan",
  abstract =     "A notation to describe software system designs is
                 given together with the means to verify properties over
                 them. De- signs are considered as models of a modal
                 logic. The pro- cedure to derive the modal model
                 associated to a design, the algorithm to check
                 properties over a model, the method to de ne new
                 relations and the method of model ltration are
                 presented. The proposed logic (KPI a poly-modal logic
                 with inverse operators) is used as a property speci
                 cation language veri ed through a model checking
                 algorithm. The methods provided proved to be e ective
                 and simple to im- plement. A prototype tool has been
                 developed in SML-NJ covering all functionalities
                 described.",
  pages =        "150--152",
  owner =        "areces",
  timestamp =    "2016.09.30",
  ISBN =         "0-8186-8439-9",
}