17, Mar, 2015 11:30-12:30 (1 hour)
CISTER, Porto, Portugal

ABSTRACT:
With the advent of always more complex computing platforms and the adoption of new computing paradigms to exploit the power of those architectures, verifying whether a system respects its functional and timing specifications became a big challenge. Static verification has proven limited either because of the state explosion problem as in the case of approaches based on model checking, or simply due to theoretical limitations of approaches based on deductive verification. Testing and simulations are often presented as solutions to improve the confidence in the final system. However, one can never ensure an exhaustive testing of all the possible situations and input scenarios. Furthermore, ensuring the correctness of extra-functional properties before the system deployment is difficult and usually subject to a high degree of pessimism, essentially because the data that must be manipulated is almost always available only at run-time, and depends on specificities of the underlying hardware, interactions with the external physical environment and interference caused by concurrent applications. Run-time verification is a complementary solution to those presented above. It consists in adding monitors in the system that gather information during the execution and check if the monitored applications behave according to predefined specifications. In case of a detected misbehavior, counter-measures can be triggered to avoid or mitigate the impact of a failure, for example, by triggering an execution-mode change, modifying the period or the priority of some tasks, adapting the task mapping on the cores or simply deactivating non-critical tasks. Because monitors use real data generated at run-time, run-time verification allows to check if the assumptions made during the analysis and development phase are respected at run-time. Although previous works on run-time verification exist, they are usually unsuited to real-time safety-critical applications. In this talk we will discuss the relevant part of the current state-of-the-art that addresses safety-critical systems, and present our own contribution to this area, which consists in a novel run-time verification architecture that defines how monitors and monitored application interact in a way that enforces both reliability and efficiency, namely by allowing an independent and composable development, enforcing time and space partitioning, and ensuring responsiveness. We will then discuss how monitors checking application properties defined in a high-level specification language, could be automatically generated in a correct-by -construction manner.

EVENT PHOTOS:
At CISTER's Facebook page

DOWNLOAD:
PDF Presentation (3.3MB)

CISTER's main roles: