Formal analysis of parametric timed systems

OData support
Supervisor:
Vörös András
Department of Measurement and Information Systems

Parametric timed systems are systems whose behavior depends on timing constrained by time parameters. These systems often operate in a safety critical environment, hence their provably correct behavior has to be guaranteed by the application of formal methods. This thesis summarizes the basics of model checking, one of the most successful formal approaches. Moreover, it presents the principles of the theory of timed, respectively parametric timed automata, which are formalisms that are suitable for modeling of such systems. Furthermore, a model based language framework is introduced, with a syntax that enables direct modeling of parametric timed behavior; together with a semantics based on a series of model transformations and mapping to a logical representation that allows the symbolic analysis of the model. The usability of the approach is demonstrated on two examples: the first one is a canonical example, Fischer's well known Mutual Exclusion Protocol, and the second one is an industrial case study, the connection handling of Prolan's SCAN protocol.

Downloads

Please sign in to download the files of this thesis.