Animating lotos specifications using AMLOG

Atsushi Togashi, Glenn Mansfield, Norio Shiratori

    Research output: Contribution to journalArticle

    Abstract

    In order to achieve a more convenient and intelligent handling of LOTOS specifications, an approach is proposed wherein specifications are translated into an appropriate equational logic language and interpreted. LOTOS has an excellent formal model for describing communication processes and equational logic languages have the capability of inferencing and data abstraction. Naturally, the marriage of LOTOS and equational logic provides a powerful framework with features that could not be realized in existing technologies. To demonstrate this potential, AMLOG is chosen as the appropriate equational logic language. Apart from rapid prototyping of specifications, some of the exciting possibilities of the new framework that are demonstrated include stepwise refinement and testing for correctness of specifications, facilities for property checking and verification of bisimulation equivalences. Also, the derivation of behavior expressions from trace histories is shown. The approach, extensible to other FDTs as well, is a step towards realizing an intelligent communication protocol specification environment.

    Original languageEnglish
    Pages (from-to)5-19
    Number of pages15
    JournalInternational Journal of Software Engineering and Knowledge Engineering
    Volume6
    Issue number1
    Publication statusPublished - 1996 Mar

      Fingerprint

    Keywords

    • AMLOG
    • Behavior equivalence
    • Equational logic language
    • LOTOS interpreter
    • LOTOS specification
    • Property checking

    ASJC Scopus subject areas

    • Artificial Intelligence
    • Computer Graphics and Computer-Aided Design
    • Software
    • Electrical and Electronic Engineering

    Cite this