Automatic analysis of embedded systems specified in Astral

A prerequisite for successful software development is the availability of a complete and consistent software requirements specification. One way to asses the correctness of requirements specifications is the application of formal verification. Recently, the verification tool Uppaal has become available. Uppaal performs automatic verification of properties of real-time systems through model-checking using timed automata. Timed automata have proved very useful in automatic analysis, but do not allow easy specification of requirements at a sufficiently high level. Astral is a formal specification language for (real-time) software requirements. Automatic analysis of specifications is very useful for generating feedback to the end-user pointing out errors in the specification or showing that it satisfies certain properties. The analysis improves the process of requirements elicitation and therefore increases Astral´s usability. The paper reports on the authors´ experiences using Uppaal for automatic analysis of Astral specifications. They discuss and evaluate a translation from Astral specifications into Uppaal´s timed automata. Particular focus is on the transformation of Astral´s maximal progress semantics into the semantic setting of the timed automata, which do not have a maximal progress semantics. They report on experience with automatic analysis of an Astral specification of the `Generalised Railroad Crossing´ example