Description
John Wiley Inverse Method/Parametric Verification Of Real-Time Unbedded Systems by André
This book introduces state–of–the–art verification techniquesfor real–time embedded systems, based on the inverse method forparametric timed automata. It reviews popular formalisms for thespecification and verification of timed concurrent systems and, inparticular, timed automata as well as several extensions such astimed automata equipped with stopwatches, linear hybrid automataand affine hybrid automata. The inverse method is introduced, and its benefits for guaranteeingrobustness in real–time systems are shown. Then, it is shown how aniteration of the inverse method can solve the good parametersproblem for parametric timed automata by computing a behavioralcartography of the system. Different extensions are proposedparticularly for hybrid systems and applications to schedulingproblems using timed automata with stopwatches. Various examples,both from the literature and industry, illustrate the techniquesthroughout the book. Various parametric verifications are performed, in particular ofabstractions of a memory circuit sold by the chipset manufacturerST–Microelectronics, as well as of the prospective flight controlsystem of the next generation of spacecraft designed by ASTRIUMSpace Transportation.