Guest lecture
Laitoksellamme vierailee 14-16.9.Vierailun yhteydessä hän pitää laitoksellamme (Teollisuuskatu 23, Helsinki, Vallila) maanantaina 14.9 kello 14--16 salissa B649 (6.kerros) tutkimusalaltaan yleiskatsausesitelmän otsakkeella: Prof. Heiko Krumm
Dortmundin yliopisto, Saksa
Formal modelling of distributed systems in cTLA
Hän pitää myös aihepiiristä (hajautettujen järjestelmien formaali spesifiointi ja verifiointi) kiinostuneille samassa salissa tiistaina 15.9 kello 14--17 ja keskiviikkona 16.9 kello 14--17 lyhyen 6 tunnin johdantoluentosarjan otsakkeella:
Specification, Design, and Verification of Distributed Applications Based on cTLA
Sekä yleiskatsausesitelmän että luentosarjan sisältötiivistelmät ovat alempana.
(TLA = Temporal Logic of Actions)Tervetuloa!
Martti Tienari
Abstract I
FORMAL MODELLING OF DISTRIBUTED SYSTEMS IN CTLA The formal specification language cTLA is based on Leslie Lamport's Temporal Logic of Actions TLA and supports the modular description of concurrent and distributed process systems. cTLA-modules define generic process types, instances can be composed to system models. In particular, a process composition coincides with the consistent logical conjunction of the process formulas. Therefore, the composition has the character of superposition, i.e., safety and liveness properties of processes are also properties of the system as a whole. Consequently, processes not only can represent implementation components but also can stand for purely logical behaviour constraints.
The talk introduces cTLA and reports on essentials of its practical application. Even the verification of very complex systems is manageable, if a suitable constraint-structured system specification exists. Then only small subsystems have to be considered in order to verify system properties of interest. This approach has been applied very successfully for the verification of data transfer protocols. Furthermore, the composition of cTLA and the refinement conception of TLA can be combined in order to support the design of systems directly. In this approach, a design step is performed by composing a refined solution pattern specification with the intermediate system specification.
Abstract II
ABSTRACT OF A SHORT LECTURE SERIES (6 lecturing hours) Distributed applications, abstract algorithms as well as detailed implementations, can be modelled formally as state transition systems. Temporal logic formulas can be applied to specify and verify safety and liveness properties. In particular, Leslie Lamport's Temporal Logic of Actions TLA has been designed to support practical applications. Our specification technique cTLA is a variant of TLA and aims specially to the modular description of distributed systems. It adds generic process types, processes, and a special process composition to TLA which are well-suited for the formal construction and analysis of practically relevant distributed systems.
The short lecture series firstly introduces into the TLA-based specification and verification techniques (e.g., state transition system model, invariants and auxiliary variables, safety and liveness proofs, refinement proofs) and into their application for the design and analysis of distributed systems. Thereafter we discuss the extensions of TLA to cTLA (e.g., process types, process instances, operations: composition, refinement, design pattern integration, and process splitting). The resulting support for the formal development of distributed applications will be exemplified. It comprises the structured formal verification of system properties as well as semantics-preserving and pattern-guided refinement steps. Finally, continuing work will be outlined.
Specification frameworks are devoted to a special field of application. They supply reusable specification elements and theorems. Moreover, extensions of cTLA address distributed real-time, continuous, and hybrid systems. Another current approach maps diagrams of object-oriented specifications (e.g., UML diagrams) into constraint-oriented cTLA-processes.