A Methodology for Constructing Correct Reactive Systems

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.