Real-time embedded systems are becoming more complex and open, making their development process extremely challenging and expensive, as well as much harder to verify and validate. Techniques like testing and simulation struggle to provide enough coverage of the system properties due increased number of reachable state of the system. Static verification methods like model checking and theorem proving also suffer from fundamental problems like state explosion problem and lack of decision procedures, namely when various of extra-functional properties (e.g., time, energy, temperature, humans-in-the-loop behaviors, etc.) involved in the system’s design. Although runtime verification is a powerful alternative to the limitations of traditional verification methods, the developments focused on the specific properties of real-time systems are quite scarce when compared to the solutions proposed for common software applications.
In this talk, we will present some of the ongoing work being done in the CISTER research center, namely, a restricted fragment of Metric Temporal Logic with Durations and the associated methods to synthesize monitors; we will also describe a software architecture that allows the monitoring of applications with strong guarantees of space and time isolation between the monitors and the monitored application. These two developments fit in two fundamental aspects of any runtime verification framework: formal specification languages and runtime monitoring architectures. The former are the tools that allow the developer to express the properties that are considered necessary to verify during the system’s run-time; the latter ensures that the monitors interact with the monitored application without compromising its original expected behavior, which otherwise could lead to unforeseen events that could lead to unrepairable (physical and monetary) losses.
----
David Pereira was born in Porto, Portugal, in 1980. In 2003 he received his degree in Computer Science at University of Porto. In 2007 he finished his Master's degree in Computer Science also in University of Porto, in the areas of formal logics for specifying and reasoning about intelligent agents. He has a PhD in Computer Science, in the MAP-i PhD program. His research is focused in the mechanisation of Kleene algebra and Kleene algebra with tests in the Coq theorem prover. He also mechanised a deductive proof system for dealing with the partial correctness of parallel programs, under the spirit of Rely/Guarantee thinking. The aim is to apply such mechanisations to conduct partial verification of correctness of both sequential and parallel imperative programs. Since he joined CISTER, David’s interests and research is focused on applying verification methods to Runtime-Verification, a lightweight formal verification approach that checks the correctness of software during execution time, and apply these approaches in the development of safe and predictable hard-real time systems.
Web-page: http://www.cister.isep.ipp.pt/people/david_pereira/