You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.

The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.

For the reports in this repository we specifically note that

  • the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at http://www.ieee.org/web/publications/rights/copyrightpolicy.html)
  • the use of articles under ACM copyright is governed by the ACM copyright policy (available at http://www.acm.org/pubs/copyright_policy/)
  • technical reports and other articles issued by M‰lardalen University is free for personal use. For other use, the explicit consent of the authors is required
  • in other cases, please contact the copyright owner for detailed information

By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.

If you are in doubt, feel free to contact webmaster@ide.mdh.se

A Methodology for Constructing Correct Reactive Systems

Fulltext:


Publication Type:

Book

Publisher:

Ph.D. thesis, Turku Centre for Computer Science, Turku, Finland


Abstract

The challenges of designing reactive systems, which are supposed to maintain an ongoing interaction with a possibly unpredictable environment, stem from the need of ensuring the correctness of the design at the earliest stage possible. An increasingly appealing mathematical approach towards accomplishing this goal is formal system construction. While enjoying the advantages of a rigorous development process, it also frees the designer from the burden of taking into account implementation details, from the beginning.This thesis proposes a formal methodology that aims at constructing correct reactive systems. Our work lies in the area of computerized systems that combine aspects of discrete control, continuous data values and real-time constraints. We address the issues from the perspective of a logical framework called refinement calculus. The results are described in terms of various forms of the so-called action systems.Designing for reactivity assumes dealing with composability and concurrency. Targeting the correct execution of concurrent actions, we introduce a synchronized semantics for the parallel composition of action systems. The construct mimics the barrier synchronization mechanism found as a primitive in concurrent programming languages. We prove that the synchronized composition improves the modular design capabilities of our framework. This translates into being able to carry out refinements of modules, modeled by action systems, in isolation, without knowledge about the details of functionality of the other modules of the parallel environment.Hybrid control systems are reactive systems characterized by continuous behavior interleaved with discrete control decisions. As a precursor to full formal analysis, simulation of hybrid system models can be used effectively, especially if the state space is represented symbolically. We present a simulation tool for continuous action systems (CAS), the timed extension of action systems. The simulator is implemented in Mathematica, a commercial computer algebra package. Our tool takes a description of any CAS as input, and provides automatically a symbolic simulation of the system, up to a given maximum time.To cope with the concurrent behavior of hybrid systems, we extend the synchronization execution environment developed for discrete action systems, to their hybrid counterparts. The modularity results at the discrete level hold for the synchronized composition of CAS, too.Many hybrid systems are defined using parameters. The systems are intended to work correctly under specific parametric conditions. These relationships may be hard to find by following an intuitive approach alone. We apply the well-known invariance rule to the parametric reachability problem of hybrid systems modeled as CAS. We synthesize constraints on parameters that are sufficient to guarantee the safety property of a relevant hybrid system example.When timing requirements are set on top of the functional ones, for any type of reactive system, be it discrete or hybrid, we need to find a means to cope with them, in design. This should be done regardless of the respective functional behavior. Being faithful to this viewpoint, we advance a top-down method for the incremental construction of scheduled real-time systems, within the refinement calculus framework. We apply the method on two well-known scheduling algorithms, namely Deadline-Monotonic and Earliest-Deadline-First policies.A viable controller construction method is known in literature as controller synthesis. Synthesis is equivalent to computing the most general model of a controller that satisfies the requirements. Here, we propose a game-based method for the synthesis of invariance and certain reachability controllers.

Bibtex

@book{Seceleanu1378,
author = {Cristina Seceleanu},
title = {A Methodology for Constructing Correct Reactive Systems},
isbn = {951-29-4015-9},
month = {January},
year = {2005},
publisher = {Ph.D. thesis, Turku Centre for Computer Science, Turku, Finland},
url = {http://www.es.mdh.se/publications/1378-}
}