TUTCRIS - Tampereen teknillinen yliopisto

TUTCRIS

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

Tutkimustuotos

Standard

Aspects of Continuous Behaviour - Design of Real-Time Reactive Systems in DisCo. / Katara, M.

Tampere : Tampere University of Technology, 2001. (Tampereen teknillinen korkeakoulu. Julkaisuja; Nro 346).

Tutkimustuotos

Harvard

Katara, M 2001, Aspects of Continuous Behaviour - Design of Real-Time Reactive Systems in DisCo. Tampereen teknillinen korkeakoulu. Julkaisuja, Nro 346, Tampere University of Technology, Tampere.

APA

Katara, M. (2001). Aspects of Continuous Behaviour - Design of Real-Time Reactive Systems in DisCo. (Tampereen teknillinen korkeakoulu. Julkaisuja; Nro 346). Tampere: Tampere University of Technology.

Vancouver

Katara M. Aspects of Continuous Behaviour - Design of Real-Time Reactive Systems in DisCo. Tampere: Tampere University of Technology, 2001. (Tampereen teknillinen korkeakoulu. Julkaisuja; 346).

Author

Katara, M. / Aspects of Continuous Behaviour - Design of Real-Time Reactive Systems in DisCo. Tampere : Tampere University of Technology, 2001. (Tampereen teknillinen korkeakoulu. Julkaisuja; 346).

Bibtex - Lataa

@book{e50a446ee170449e9698ac56a3e8156b,
title = "Aspects of Continuous Behaviour - Design of Real-Time Reactive Systems in DisCo",
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.",
author = "M. Katara",
note = "Awarding institution:Tampere University of Technology",
year = "2001",
language = "English",
series = "Tampereen teknillinen korkeakoulu. Julkaisuja",
publisher = "Tampere University of Technology",
number = "346",

}

RIS (suitable for import to EndNote) - Lataa

TY - BOOK

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

AU - Katara, M.

N1 - Awarding institution:Tampere University of Technology

PY - 2001

Y1 - 2001

N2 - 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.

AB - 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.

M3 - Doctoral thesis

T3 - Tampereen teknillinen korkeakoulu. Julkaisuja

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

PB - Tampere University of Technology

CY - Tampere

ER -