|CHIARI MICHELE||Cycle: XXXIV |
Section: Computer Science and Engineering
Tutor: MIRANDOLA RAFFAELA
Advisor: MANDRIOLI DINO Major Research topic
:Temporal Logic and Model Checking for Operator Precedence Languages: Theoretical and Practical ApplicationsAbstract:
The growing ubiquity of computer systems in every industrial sector has posed increasingly demanding challenges, one of the most crucial being the verification of adherence of mission- and safety-critical systems to their requirements. One of the most successful and popular techniques that have been developed for this objective is model checking. It consists in the formal specification of the system’s requirements by means of a logic formalism, in the generation of a model of the system in exam by using an operational or denotational formalism, and in the subsequent automatic and exhaustive verification of the adherence of the latter to the former.
The capabilities of this process depend on the choice of the formalisms mentioned above. The most classical thereof are Linear Temporal Logic (LTL), Computation Tree Logic (CTL) and CTL*. In particular, LTL maintains the same expressive power of First-Order logic (FO), while providing a model-checking procedure which is only exponential in the size of the specification, and not non-elementary as FO. However, LTL only allows to express properties in the realm of regular languages: indeed, its model-checking procedure is based on Finite State Automata.
Recently, the literature has seen considerable efforts in the direction of extending the expressive power of temporal logic towards larger language classes. The most notable of them is the work on temporal logics based on Visibly Pushdown Languages (VPL), which led to the introduction of the logic CaRet, and of the First-Order complete NWTL. VPL are a subclass of Deterministic Context-Free languages (DCFL), and they are only slightly more expressive than parenthesis languages.
In this context, the thesis investigates the possibility of developing a model-checking framework based on Operator Precedence Languages (OPL). OPLs, which are also a subclass of DCFLs, are significantly more expressive than VPLs and, consequently, regular languages. Being suitable to describing the syntax of real-world programming languages, they could dramatically extend the properties expressible in system specifications. In this thesis, we present different temporal logic formalisms capable of expressing OPL properties. Furthermore, we provide an effective procedure that enables model-checking properties and systems based on such formalisms. We then investigate the feasibility of an actual implementation, as well as its applicability in real-world scenarios.