Hard real-time software such as automobile and airplane control software consists of many concurrent processes and many states, and especially timing constraints are strict. It is necessary to model, specify and verify hard real-time software including timing constraints. As noted in Kavi13, there are many development methods and specification methods such as real-time structured analysis and Petri nets, automaton, process algebras, temporal logic, timed Petri nets, timed automaton, timed process algebra and real-time temporal logic. But there are many problems such as lack of modeling techniques, understandability and documentability.
展开▼
