An approach towards formal verification of object oriented real-time systems

This paper describes an approach towards verification of object oriented real-time software systems, based on ATL+, a formal specification language of which the syntax and semantics are inspired by the Java programming language. Using a specification language based on an object oriented programming language reduces the semantic gap between the implementation of a system and the model used for verification. We describe the syntax and semantics of ATL+, as well as a transformation procedure by which ATL+ is transformed into a notation suitable for use with an automated verification tool. We show the applicability of our method by giving some verification results, in which properties and constraints on design parameters are derived for a simple example