Formal specification and refinement of a safe train control function

Motivated by the design and development challenges of the BART case study, an approach for developing and analyzing a formal model for reactive systems is presented. The approach makes use of a domain specific language for specifying control algorithms able to satisfy competing properties such as safety and optimality. The domain language, called SPC, offers several key abstractions such as the state, the profile, and the constraint to facilitate problem specification. Using a high-level program transformation system such as HATS being developed at the University of Nebraska at Omaha, specifications in this modelling language can be transformed to ML code. The resulting executable specification can be further refined by applying generic transformations to the abstractions provided by the domain language. Problem dependent transformations utilizing the domain specific knowledge and properties may also be applied. The result is a significantly more efficient implementation which can be used for simulation and gaining deeper insight into design decisions and various control policies. The correctness of transformations can be established using a rewrite-rule based induction theorem prover Rewrite Rule Laboratory developed at the University of New Mexico.

A REACHABILITY TREE FOR STATECHARTS AND ANALYSIS OF SOME PROPERTIES

Statecharts are an extension to finite state machines with capability for expressing hierarchical decomposition and parallelism. They also have a mechanism called history, to remember the last visit to a superstate. An algorithm to create a reachability tree for statecharts is presented. Also shown is how to use this tree to analyse dynamic properties of statecharts; reachability from any state configuration, usage of transitions, reinitiability, deadlocks, and valid sequence of events. Owing to its powerful notation, building a reachability tree for statecharts presents some difficulties, and we show how these problems were solved in the tree we propose.

Phasenverhalten von Polyethylen in Mischsystemen

Die vorliegende Arbeit besch��ftigt sich mit dem Phasenverhalten von Polyethylen (PE) in nicht-reaktiven und in reaktiven Systemen. Von drei eng verteilten Polyethylenen (Mw = 6,4, 82 bzw. 380 kg/mol) in n-Hexan sowie f��r das System 2,2-Dimethylbutan / PE 82 wurde die Entmischung in Abh��ngigkeit von der Zusammensetzung, dem Druck und der Temperatur experimentell bestimmt. Die Modellierung der Tr��bungskurven erfolgte nach der Theorie von Sanchez und Lacombe. Dieser Ansatz beschreibt die Ergebnisse qualitativ und kann in einem engen Temperatur- und Druckbereich f��r gegebenes Molekulargewicht die kritische Temperatur und den kritischen Druck quantitativ vorhersagen. Durch Extrapolation der kritischen Temperatur der verschiedenen L��sungen von PE in n-Hexan auf unendliches Molekulargewicht nach Shultz-Flory wurde im Druckbereich von 20 bis 100 bar und im Temperaturbereich von 130 bis 200 ��C eine Grenzlinie bestimmt. Diese Linie trennt unabh��ngig vom Molekulargewicht des Polymers und der Zusammensetzung der Mischung das Zweiphasengebiet vom homogenen Bereich. Im Fall des Mischl��sungsmittels n-Hexan / 2,2-Dimethylbutan wurde f��r eine ann��hernd kritische Polymerkonzentration die Abh��ngigkeit der Entmischungsbedingungen von der Zusammensetzung untersucht. Durch einfache Erweiterung der Sanchez-Lacombe-Theorie und Einf��hren eines Fitparameters konnte das tern��re System beschrieben werden. An einer breit verteilten PE-Probe wurden Experimente zur Fraktionierung von PE in n-Hexan durchgef��hrt. Die Analyse der in den koexistenten Phasen enthaltenen Polymere lieferte Informationen ��ber die Konzentration und die Molekulargewichtsverteilung des PE in diesen Phasen sowie die kritische Zusammensetzung der Mischung. Von verschiedenen PE-L��sungen (Mw = 0,5 kg/mol) wurde die polymerisationsinduzierte Phasenseparation in Isobornylmethacrylat mit und ohne Vernetzer untersucht. Mit 15 Gew.-% PE und in Abwesenheit von Vernetzer findet die Entmischung erst bei hohen Ums��tzen statt. Die Charakterisierung der resultierenden Proben zeigte, dass sich etwas mehr als 5 Gew.-% PE im Polyisobornylmethacrylat l��sen. Die Glas��bergangstemperaturen der Polymermischungen steigen mit steigender Vernetzer- und sinkender Polyethylenkonzentration. Bei Proben mit 15 Gew.-% PE zeigte sich folgendes: 5 Gew.-% Vernetzer f��hren zu gro��en PE-Bereichen (150 - 200 nm) in der Matrix und der Kristallinit��tsgrad ist gering. Bei der Polymermischung mit 10 Gew.-% Vernetzer bilden sich sehr kleine Polyethylenkristalle (< 80 nm) und der Kristallinit��tsgrad ist hoch. Ohne Vernetzer h��ngt der Kristallinit��tsgrad - wie bei reinem PE - von der Abk��hlrate ab, mit Vernetzer ist er von ihr unabh��ngig.

Verifying data refinements using a model checker

In this paper, we consider how refinements between state-based specifications (e.g., written in Z) can be checked by use of a model checker. Specifically, we are interested in the verification of downward and upward simulations which are the standard approach to verifying refinements in state-based notations. We show how downward and upward simulations can be checked using existing temporal logic model checkers. In particular, we show how the branching time temporal logic CTL can be used to encode the standard simulation conditions. We do this for both a blocking, or guarded, interpretation of operations (often used when specifying reactive systems) as well as the more common non-blocking interpretation of operations used in many state-based specification languages (for modelling sequential systems). The approach is general enough to use with any state-based specification language, and we illustrate how refinements between Z specifications can be checked using the SAL CTL model checker using a small example.

Continuous action system refinement

Action systems are a framework for reasoning about discrete reactive systems. Back, Petre and Porres have extended these action systems to continuous action systems, which can be. used to model hybrid systems. In this paper we define a refinement relation, and develop practical data refinement rules for continuous action systems. The meaning of continuous action systems is expressed in terms of a mapping from continuous action systems to action systems. First, we present a new mapping from continuous act ion systems to action systems, such that Back's definition of trace refinement is correct with respect to it. Second, we present a stream semantics that is compatible with the trace semantics, but is preferable to it because it is more general. Although action system trace refinement rules are applicable to continuous action systems with a stream semantics, they are not complete. Finally, we introduce a new data refinement rule that is valid with respect to the stream semantics and can be used to prove refinements that are not possible in the trace semantics, and we analyse the completeness of our new rule in conjunction with the existing trace refinement rules.

Semantic properties of ��-charts

��-Charts are a Statechart-like language which is designed for specifying reactive systems. This paper extends the language of ��-charts with a new parallel operator; it defines a formal semantics for the language, and then it explores the semantic properties of the extended language. The paper concludes with a simple case study to illustrate how the language may be used to specify and reason about reactive systems.