Aspects of Continuous Behaviour - Design of Real-Time Reactive Systems in DisCo

M. Katara

    Research output: Book/ReportDoctoral thesis

    23 Downloads (Pure)

    Abstract

    Reactive systems, i.e. those in constant interaction with their environments, are often distributed entailing concurrency. Real time is a continuous quantity used to model timing constraints of reactive systems. Developing real-time reactive systems is a battle against complexity. To win this battle methods are needed which support the specification process as well as the validation and verification of specifications. In this thesis an approach concentrating on these important development phases is presented. The foundation of the approach is DisCo which is a formal method for distributed reactive systems. The formal basis of DisCo is in the Temporal Logic of Actions by Lamport. At the core of DisCo are the joint action theory and the closed system principle enabling capturing of collective behaviour of objects before defining their interfaces. Moreover, layered design based on superposition enables effective separation of concerns. The approach contributes to the specification of real-time systems by introducing generic real-time events and a mechanism for their utilization in specifications. Furthermore, the structuring of specifications is elaborated in the light of aspect-orientation, a methodology inspired by the identification of cross-cutting design concerns that do not fit into any single existing unit of modularity, for instance a class. Moreover, the constructs for modelling real time can be generalized to other continuous quantities as well. An example is presented where locations of mobile devices are also of concern. To advance the development of not only well structured but also correct specifications, tools for validation of real-time specifications are presented. A mapping from finite instantiations of DisCo specifications into timed automata is also described. The mapping enables automatic verification of real-time specifications using an existing model checking tool.
    Translated title of the contributionAspects of Continuous Behaviour - Design of Real-Time Reactive Systems in DisCo
    Original languageEnglish
    Place of PublicationTampere
    PublisherTampere University of Technology
    Publication statusPublished - 2001
    Publication typeG5 Doctoral dissertation (article)

    Publication series

    NameTampereen teknillinen korkeakoulu. Julkaisuja
    PublisherTampere University of Technology
    No.346

    Publication forum classification

    • No publication forum level

    Fingerprint

    Dive into the research topics of 'Aspects of Continuous Behaviour - Design of Real-Time Reactive Systems in DisCo'. Together they form a unique fingerprint.

    Cite this