Faculty of Science, Technology and Medicine
Faculty of Law, Economics and Finance
Faculty of Humanities, Education and Social Sciences
Interdisciplinary Centre for Security, Reliability and Trust
Luxembourg Centre for Systems Biomedicine
Luxembourg Centre for Contemporary and Digital History
Luxembourg Centre for European Law
Luxembourg Centre for Socio-Environmental Systems
The Doctoral School in Science and Engineering is happy to invite you to Cristina STRATAN’s defence entitled
Diagnostics of iCFTL source code specification violations
Supervisor: Assoc. Prof Domenico BIANCULLI
As modern software systems grow in complexity and operate in dynamic environments, the need for runtime analysis techniques becomes a more critical part of the verification and validation process. Runtime Verification (RV) is a lightweight formal method that monitors whether an execution trace—a sequence of recorded events—satisfies a given specification. Traditionally, RV produces Boolean or quantitative verdicts to express whether an execution satisfies or violates a specification.
When a specification is violated, such a verdict is often insufficient to understand why the violation happened. To address this limitation, diagnostics approaches enrich the verdict by identifying and presenting the minimal or most relevant segments of the execution trace, together with the corresponding elements of the specification, that explain why a verdict was produced.
This thesis proposes a diagnostics approach for Inter-procedural Control-Flow Temporal Logic (ICFTL), a specification language designed to capture properties related to the inter-procedural, source-code-level behavior of programs.
The contributions of this thesis are:
- A diagnostics approach for time-based ICFTL specifications. This approach computes a segment of an execution trace up to the event after which the specification becomes impossible to satisfy, thereby helping engineers identify and diagnose performance-related issues in the code.
- A diagnostics approach for state-based ICFTL specifications. This approach uses backward data-flow analysis to trace how variable values are computed across procedures and statements, helping engineers understand how the data-flow contributed to the state-based specification violation.
- An approach for computing a core diagnosis: a set of program points consolidated from the diagnosis of a violated specification, obtained by removing redundant information and highlighting only the most relevant program points. This provides engineers with a clear overview of the diagnosis.