Formal Requirements Analysis and Specification-Based Testing in Cyber-Physical Systems

Formal requirements analysis plays an important role in the design of safety- and security-critical complex systems such as, e.g., Cyber-Physical Systems (CPS). It can help in detecting problems early in the system development life-cycle, reducing time and cost to completion. Moreover, its results can be employed at the end of the process to validate the implemented system, guiding the testing phase. Despite its importance, requirements analysis is still largely carried out manually due to the intrinsic difficulty of dealing with natural language requirements, the most common way to represent them. However, manual reviews are time-consuming and error-prone, reducing the potential benefit of the requirement engineering process. Automation can be achieved with the employment of formal methods, but their application is still limited by their complexity and lack of specialized tools. In this work we focus on the analysis of requirements for the design of CPSs, and on how to automatize some activities related to such analysis. We first study how to formalize requirements expressed in a structured English language, encode them in linear temporal logic, check their consistency with off-the-shelf model checkers, and find minimal set of conflicting requirements in case of inconsistency. We then present a new methodology to automatically generate tests from requirements and execute them on a given system, without requiring knowledge of its internal structure. Finally, we provide a set of tools that implement the studied algorithms and provide easy-to-use interfaces to help their adoption from the users.