Contract-based specification of embedded control systems
Oguzcan Oguz is a PhD Student in the reseach group Formal Methods and Tools. His Supervisor is Professor Jaco van de Pol from the Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS).
In this thesis our overall aim is to provide a contract-based embedded system development process with an emphasis on specification and analysis. We specify components and layers via assume/guarantee contracts and use a contract algebra as the backbone to supply necessary operations to compose, refine and validate contracts. We employ various modelling formalisms, such as timed automata and hybrid automata to express contracts. The choice of the formalism is made according to the sort of behaviours of the component at hand. We employ appropriate model-based analysis methods, such as model checking and simulation, to support practical contract operations.
Our first contribution is a contract-based specification architecture and the associated process. The specification architecture is mode based where a system is specified with a number of operational modes and a mode-switching logic. The concrete formalisms used are based on timed automata for switching logic and hybrid automata for specification of individual modes. Practical methods for composing and analysing hybrid automata-based contracts are defined over using hybrid observers which enable employing hybrid system simulation tools. To analyse timed automata-based contracts in isolation, model checking is employed. Specific validity criteria for mode and switching components are defined for each step of the specification process.
Our second contribution is a method to use timed automata-based specifications as observers in a hybrid system simulation tool. We provide the associated implementation which employs Uppaal model-checking tool to execute such generic timed automata-based specifications alongside hybrid automata based-observer specifications. In the context of the described specification process, this enables validating contracts with assertions expressed in both timed and hybrid automata.
Our third contribution is a generic schedulability framework using model checking on timed-CSP models. The framework enables analysing multiprocessor schedulability of CSP models with non-preemptive fixed-priority tasks with variable execution times. We present a schedulability analysis workflow that describes how to utilize the proposed framework in a generic CSP-based design process. We also describe how to integrate the schedulability framework to a contract-based design process.
