Dr. Mark Lawford, Mc Master University spoke at the UCD CASL on Tuesday, the 19th of June 2007.Formal Verification of Implementability of Timing Requirements
While there has been a large amount of work on validation of timing requirements, there has been relatively little work on the implementability of timing requirements. In this talk we provide definitions of fundamental timing operators that explicitly considered tolerances on property durations and intersample jitter. We have modeled and formalized the analysis of one of the operators in the PVS theorem prover. The first result is a formal proof of necessary and sufficient conditions for when it is possible to meet the requirement with a discrete implementation with bounded variation in sampling times.
Mark is an Associate Professor in the Department of Computing And Software at McMaster University. Mark's research interests fall under the general headings of Software Engineering and Control of Discrete Event Systems (DES), in particular Formal Methods for Real- Time Systems (synthesis, verification, and model reduction), practical application of formal methods in the software engineering process, computer aided inspection, and supervisory control of modular, nondeterministic and probabilistic DES, and hybrid systems.