A real-time specification method for specifying and validating real-time concurrent systems

A real-time specification method is presented for specifying and validating the behavior of real-time concurrent software systems. The method consists of the Descartes-RT specification into an extended Petri net. Descartes-RT is a formal language, which is an extension of the executable Descartes specification language for sequential systems. Communicating processes specified by Descartes-RT use local data for modifying and transmitting shared information. A timer as a Descartes specification module is used to impose timing constraints on concurrent processes for synchronization and lossless data transmission between concurrent processes. The execution sequence and timing constraints of a specification for a concurrent system are converted into an extended Petri net model which is used to analyze the correctness of the specified software. The analysis is focused on the safety and liveness of concurrent processes. Those properties of concurrent systems can be examined and proved by inspecting the movement of tokens