Real-time systems: formal specification and automatic verification

摘要

The authors' stated-and well-achieved-purpose for this advanced and highly focused book on formally specifying and automatically verifying real-time embedded safety-critical systems is to bring together duration calculus (DC), timed automata, and programmable logic controller (PLC) automata, so as "to form a seamless design flow, from realtime requirements specified in the duration calculus, via designs specified by PLC-automata, and into source code for hardware platforms of embedded systems."