• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Stepwise Development of Hybrid Systems

Mauno Rönkkö, Stepwise Development of Hybrid Systems. TUCS Dissertations 35. Turku Centre for Computer Science, 2001.

Abstract:

To assist development of computer controlled dynamical
systems we propose a stepwise development method. The
method supports development of systems with certain specified
objectives. In particular, the method supports development of
systems where the controlled object has continuous-time dynamics
although the controller has discrete-time dynamics. Such systems
are called hybrid systems.

Development of formal models for hybrid systems that satisfy
certain specified objectives, i.e., are provably correct, is intricate.
It is impossible to find an algorithm that verifies an arbitrary
property of an arbitrary hybrid system model, in general
properties are undecidable. We work around this problem
by adapting a stepwise development method for hybrid
systems. The idea of the method is to guarantee the
correctness of the system by developing it in a provably
correct stepwise manner. Thus, we start with a very simple
and provably correct abstract model, and add details to that
model one by one. For each added detail we show that
correctness is preserved. In this way, when we have
obtained a final model, we know that it is correct.

The contribution of this thesis is to provide a uniform
and systematic method for stepwise development of
hybrid systems. The method is based on results that
we have already published. However, this thesis is the
first publication that discusses how the results are used
systematically.

BibTeX entry:

@PHDTHESIS{phdRonkko01a,
  title = {Stepwise Development of Hybrid Systems},
  author = {Rönkkö, Mauno},
  number = {35},
  series = {TUCS Dissertations},
  school = {Turku Centre for Computer Science},
  year = {2001},
  keywords = {hybrid systems, predicate transformers, action systems, refinement calculus, concurrency},
  ISBN = {951-29-2043-3},
}

Edit publication