Bachelor and Master Theses
To apply for conducting this thesis, please contact the thesis supervisor(s).
| Title: | From Natural Language to Formal Verification – A Use Case on Timed Automata |
| Subject: | Computer science, Software engineering |
| Level: | Advanced |
| Description: |
Comprehensive and just-in-time design & verification of embedded systems is critical to achieve productivity and time-to-market objectives. Formal verification is a renowned approach that deals with the assessment of the correctness of a system design via formal (often mathematical) models. There exists a plethora of different formalisms for formal verification, like timed automata, petri nets etc. Verification properties are commonly specified in temporal logics, like, Computation Tree Logic (CTL), Linear Temporal Logic (LTL). Although formal verification enables timely design verification, it is a complex activity that requires domain expertise. Therefore, it is hard to reach consensus between the involved technical and non-technical stakeholders. This not only leads to several loopholes in the verification process, but also delays the overall system development. In this thesis, the aim is to provide the foundations for automating formal verification by exploiting the concepts of Natural Language Processing (NLP). More specifically, the goal is to automatically generate formal models and properties from plain textual requirements. Timed Automata (TA) will be used for demonstration purposes. TA is a well-known formalism that provides several concepts, like location, initial location, accepting location, clock, edge / switch and action for the specification of system design. Furthermore, it allows the specification of verification properties using a CTL subset. The aim is to provide an approach able to generate both system design (in TA) and properties (in CTL) from natural language requirements. Subsequently, the UPPAAL tool will be used for formal verification. The following tasks will be performed during thesis: 1) Timed Automata and UPPAAL basics 2) Natural Language Processing basics 3) Literature Review 4) Definition of Natural Language Processing rules 5) Definition of transformation rules for Timed Automata 6) Implementation & Validation 7) Thesis report writing Supervisor(s): Muhammad Waseem Anwar, Federico Ciccozzi Examiner: Antonio Cicchetti |
| Start date: | |
| End date: | |
| Prerequisites: | Good knowledge of English grammar is essential. Object-oriented programming skills are desirable. The student(s) will work on different tools and APIs e.g. UPPAAL, Eclipse / NetBeans, OpenNLP, JRegex etc. |
| IDT supervisors: | |
| Examiner: | |
| Comments: | |
| Company contact: |