An application of structural modeling and automated reasoning to real-time systems design

This paper presents an application of structural modeling and automated reasoning as a software development environment for real-time systems. This application satisfies two major requirements for such an environment: (1) to synthesize an absolutely correct program and, (2) to increase software productivity. The real-time systems, which consist of concurrent programs, are described by a Prolog based concurrent object-oriented language, called MENDEL/87. As a typical concurrent program consists of two parts: functional and synchronization parts; the functional part in the reusable component to be registered in a library will be generated by a structural modeling through the use of structuring functions with respect to data flows. The synchronization part will be synthesized from temporal logic specifications by the use of an automated reasoning mechanism. This paper also describes the MENDELS ZONE implemented on a Prolog machine, which is the working base for the presented application method.