Animating lotos specifications using AMLOG

Atsushi Togashi*, Glenn Mansfield, Norio Shiratori

*Corresponding author for this work

    Research output: Contribution to journalArticlepeer-review

    1 Citation (Scopus)


    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
    Issue number1
    Publication statusPublished - 1996 Mar


    • 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


    Dive into the research topics of 'Animating lotos specifications using AMLOG'. Together they form a unique fingerprint.

    Cite this