A framework for transforming SOFL formal specifications to programs

摘要

The SOFL (Structured Object-Oriented Formal Language) formal engineering method is developed to overcome the deficiencies of existing formal methods and to provide both rigorous and practical techniques for building formal specifications, transforming specifications to programs, and verifying both specifications and programs. Although it has been applied to system modeling and design in both industrial and research projects, SOFL has not been widely applied to the industrial software development systems because of the lack of efficient tool support. In order to improve the functions of SOFL supporting tool and solve the problem that the formal specifications could not be directly executed, the automatic transformation from formal specifications to programs is an essential part. This paper firstly analyzes the relationship between the structures of SOFL formal specifications and Java programs, and then discusses the design and implementation of the automatic transformation. Lastly, a test for ensuring the reliability of the implemented software system is discussed.