Validating specifications of dynamic systems using automated reasoning techniques

Remco Feenstra, J.C. Bioch (Editor), Roelf J. Wieringa, Y.H Tan (Editor)

    Research output: Contribution to conferencePaper

    16 Downloads (Pure)

    Abstract

    In this paper, we propose a new approach to validating formal specifications of observable behavior of discrete dynamic systems. By observable behavior we mean system behavior as observed by users or other systems in the environment of the system. Validation of a formal specification of an informal domain tries to answer the question whether the specification actually describes the intended domain. This differs from the verification problem, which deals with the correspondence between formal objects, e.g. between a formal specification of a system and an implementation of it. We consider formal specifications of object-oriented dynamic systems that are subject to static and dynamic integrity constraints. To validate that such a specification expresses the intended behavior, we propose to use a tool that can answer reachability queries. In a reachability query we ask whether the system can evolve from one state into another without violating the integrity constraints. If the query is answered positively, the system should exhibit an example path between the states; if the answer is negative, the system should explain why this is so. An example path produced by the tool can be used to produce scenarios for presentations of system behavior, but can also be used as a basis for acceptance testing. In this paper, we discuss the use of planning and theoremproving techniques to answer such queries, and illustrate the use of reachability queries in the context of information system development.
    Original languageUndefined
    Pages105-114
    Number of pages10
    Publication statusPublished - Jun 1995
    Event7th Dutch Conference on Artificial Intelligence, NAIC 1995 - Erasmus University, Rotterdam, Netherlands
    Duration: 22 Jun 199523 Jun 1995
    Conference number: 7

    Conference

    Conference7th Dutch Conference on Artificial Intelligence, NAIC 1995
    Abbreviated titleNAIC
    CountryNetherlands
    CityRotterdam
    Period22/06/9523/06/95

    Keywords

    • EWI-10648
    • IR-76204
    • SCS-Services

    Cite this

    Feenstra, R., Bioch, J. C. (Ed.), Wieringa, R. J., & Tan, Y. H. (Ed.) (1995). Validating specifications of dynamic systems using automated reasoning techniques. 105-114. Paper presented at 7th Dutch Conference on Artificial Intelligence, NAIC 1995, Rotterdam, Netherlands.