SOFTWARE ENGINEERING IN CONTROL SYSTEMS
COMPOSITIONAL SPECIFICATION AND VERIFICATION OF HYBRID SYSTEMS
The research on hybrid systems is focused on formal techniques, on defining semantics of hybrid systems specification languages with different level of abstraction, on defining design refinement operators, and on studying the correctness of corresponding proof rules. Results of the research are implemented in theorem proving environment PVS which allows systematic representation of results in form of an axiomatic theories. Another implementation is an interpreter for interval logic formulas which forms a part in model checking environment. This Prolog interference engine based model checking environment is meant for solving reachability and safety problems with different functional and timing constraints. The environment is applied for specification of experimental data reached from brain measurements (PET scans, rCBF data, etc.), testing coherence of experimental data with model experiments, formulating new hypothesis and planning experiments. Integrating the model checking environment with simulator of dynamics of LCL-arrays (lower level brain models) is in progress.
STAFF
- Jüri Vain, Ph.D.
- Marko Kääramees, Ph.D. student
- A. Sulling, J-P. Ernits, L.Lubi - students
PARTNERS IN EUROPE
- Eindhoven University of Technology
- Tampere University of Technology
- Technical University of Denmark
MATHEMATICAL AND IT METHODS FOR OPTIMAL STRUCTURIZATION OF CONTROL SYSTEMS
Research comprises classification methods for structural optimization of complex control laws and relevant control software, application of the methods in conceptual clustering of data in integrated manufacturing and information systems. New technique which combines analytical methods with clustering algorithms allows to increase the efficiency of specification in practical applications like in requirements elicitation and structurization, data and action refinement in integrated systems design and others. There are about 10 references about practical use of the technique, e.g. for power supply and distribution system design, integrated manufacturing system analysis, office information system requirements capturing, and others.
STAFF
- Tiit Riismaa, Ph.D.
- Ingmar Randvee, Ph.D.
- Mati Littover