The Saml language consists of several modeling features, like qualitative and quantitative elements, templates or failure components. They enables the engineer to easily models with systems with different apspects as well as for a wide range of analyzis. To evaluate the praticability of our language and VECS, we modeled several case studies.
Some of them, which (we think) presents best the different apsects and the processable complexity, are given here.
(For a more detailed survey of the Saml language features click here)
The Airbag Case Study is a common example of a reactive system. It therefor demonstrates how a system can be embedded in an environmental system and enhanced with failure modes. The system is composed of two sensors, which are validated by a central component. The information is processed further by two independent crash detectors and forwarded to a monitor who decided, whether the airbag is ignited or not.
In 2002, Hamburg finished the fourth tunnel of the Elbtunnel (tunnel in the west of the city) which should mitigate the traffic density on this track. Because OHV's (overhigh vehicles - higher than 4m) as trucks couldn't pass thetunnel up to then, this tunnel is constructed in the way, that these vehicle can pass it, as well
Radio-Controlled Railroad Crossing
The "Radio-Controlled Railroad Crossing"-system describes a decentral and autonomic closing and opening of a railroad barrier at railroad crossings if a train is nearing this crossing. This is it, that this system (illustrated in the picture above) extends the railroad barrier with a control system for closing and opening the barrier (Control_Track) and the train with a control system for accelerating/decelerating (Control_Train_AccDec) the train as well as determining the position of the train on the track (Determine_Train_Pos). Both, the track and the train exchange these information via a radio communication (Comm_Rad).
Landing Gear System
The landing gear system specification by Boniol et al. is a proposed benchmark for comparing and evaluating different formal model checking approaches. The Landing gear system is the safety critical part of an aircraft and have to maneuver the gears
The PZB (inductive train protection) is a system that forces trains to a standstill in case of driving too fast towards a stop. A running train is influenced by the interaction of magnets on the track and within the train.
The European Train Control System (ETCS) is an uniform European rail traffic management system designed to replace the many incompatible safety systems currently used by European railways. ETCS is based on on cab signalling and spot and/or continuous track to train data transmission. Instead of lineside signals, a computer in the driver's cab controls the speed and movement of the train, whilst taking account of other trains on the railway. ETCS is specified at four different levels (0-3) which are downward compatible.