|Title:||Formal specification of timing requirements in vehicular industry|
|Subject:||Computer science, Embedded systems|
Many embedded systems in vehicles have timing requirements. These requirements can sometimes be complex. Common practice in industry is to specify these informally, as text. This however has some disadvantages: the requirement specifications can be ambiguous, and it is also a hindrance to an automated treatment of the requirements.
This MSc project will explore different possible formal notations that can be used for specifying timing requirements in an exact manner. Candidates can be different logics, like for instance LTL that is used for model checking, the logic that underlies the TADL2 timing constraint language, or the Clock Constraint Specification Language (CCSL) defined in the UML profile for MARTE for modeling and analysis of real-time systems. Also the constraint language TADL2 itself is a candidate.
The alternative notations will be evaluated by trying to use them to express a sample of existing timing requirements, written by Scania engineers. Some evaluation criteria will be:
1. How readable and easy to understand will the requirements be for the engineer, when expressed in the notation?
2. How amenable is the notation for automation? For instance, does it allow verification methods to be used to verify automatically that the systems meet their timing requirements? Or can it be used to aid the generation of test cases?
3. How apt is the notation for expressing timing requirements together with automata?
The work will be carried out at Scania in Södertälje.
|Prerequisites:||Strong background in Computer Science. Knowledge of logic (in particular first-order predicate logic, and temporal logic). Knowledge of real-time systems.|
|IDT supervisors:||Björn Lisper, firstname.lastname@example.org|
|Company contact:||Scania Christian Lidström, email@example.com|