@TECHREPORT{R-96-41,
PSURL = {/publications/cgi-bin/tr-fetch.pl?r-96-41+ps},
ABSTRACTURL = {/publications/cgi-bin/tr-fetch.pl?r-96-41+abstr},
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.


},
NUMBER = {R-96-41},
INSTITUTION = ida,
ADDRESS = idaaddr,
YEAR = {1996},
AUTHOR = {Nadjm-Tehrani, Simin and Str{\"o}mberg, Jan-Erik},
EMAIL = {snt@ida.liu.se},
TITLE = {JAS-95 Lite: Modelling and Formal Analysis of Dynamic Properties
}