IDA Dept. of Computer and Information science, Linköping University

IDA Technical Reports: abstract

Generated: Tue, 23 Jan 2018 11:00:05

Nadjm-Tehrani, S. and Strömberg, J.-E. (1996). JAS-95 Lite: Modelling and Formal Analysis of Dynamic Properties. Technical Report LiTH-IDA-R-96-41, Department of Computer and Information Science, Linköping University, Sweden. (bibtex),

Abstract: In this report we present the multi-disciplinary work performed in the first phase of the COHSY project concerning generation of models and analysis of {\em hybrid} systems -- mathematical models including both continuous and discrete elements. The participants of the project were SAAB Military aircraft, Volvo aerospace, and VOAC hydraulics, as well as three departments from Linköping University: Computer Science, Electrical engineering and Mechanical engineering. The report addresses modelling and formal verification of a fictitious system, the landing gear of an aircraft referred to as JAS-95 Lite, which involves hydro-mechanical and electro-mechanical sensors and actuators as well as electronic and software modules performing diagnosis and control. The technical system, is moreover in dynamic interaction with a human operator (the pilot). The main aim of this work has been to mathematically prove that specified requirements are satisfied by given design specifications for the controller and alternative models for the physical environment. An architectural model is used to facilitate the combination of alternative configurations. The report provides a summary of several tracks of activity, a major one being the application and illustration of state of the art techniques in physical modelling of the hardware, and mathematical modelling and verification of the closed loop system. The languages used for modelling range from engineering schematic diagrams to Bond Graphs, hybrid transition systems, hybrid automata, and the temporal logic Extended Duration Calculus. It also provides some insights into modelling in synchronous languages for high level specification of real-time programs -- the interest being the investigation of the applicability of tools available for analysis and subsequent code generation from high level designs. Two languages from this family are examined in the context of the case study: discrete models in Esterel and timed models in statecharts as implemented in the tool Statemate.

Goto (at Linköping University): CS Dept TR Overview