From UML State Machines to Verifiable Lotos Specifications

The theoretical prospect of Formal specification languages has been improved during last years. The pragmatic aspects of the formal methods has been scrutinized especially in the safety-critical systems. However there still remains a constant fear among industry practitioners to work with purely theoretical specification methods even though their software system operates in highly safety-critical applications. We propose a hands-on approach in order to gradually transform popular UML 2.0 State Machines (SM) to verifiable Lotos specifications. In this algorithm the partial logical view of the system,represented by the UML 2.0 SM, would be converted to verifiable Basic Lotos specification, it then may be developed as an executable program to mechanize the transformation.