Abstract :
Embedded microprocessors and associated hardware resources constitute over 90% of the computing systems in use and a large number of these embedded systems are deployed in safety-critical monitoring and control applications. These embedded systems run real-time applications which must satisfy logical correctness, timing, power, and reliability constraints. They range from traditional stand-alone systems to highlynetworked cyber-physical systems, spanning a diverse array of hardware/software architectures and control models. Examples include automobile adaptive braking, industrial robotic assembly, medical pacemakers, autonomous (ground, air, and sea) vehicular travel, remote surgery, physical manipulation of nano-structures, and space exploration. Since all these embedded systems interact directly with the physical world and often have humans in the loop, their physical safety must be guaranteed. Obviously, the correctness of these embedded and cyber-physical systems depends not only on the actions or results they generate, but also on the time at which these actions are performed. The goal of this special issue is to present state-of-the-art techniques and tools for the formal specification and verification of embedded systems (hardware, software, and the environment in which these systems are embedded) so that their safety and performance can be guaranteed before they are deployed on target platforms.
