Applying Integrated Formal Methods on CPS Design

摘要

Due to the Cyber-Physical Systems (CPS) complexity its design process requires strong guarantees that the specified functional and non-functional requirements are satisfied on the designed application. Aiming to validate the specified system properties, verification techniques should be applied into the design process in order to confront such properties against the system models under development. In this context, a verification process involving the application of Model Checking, Runtime Verification, and analysis of software behavior is presented in this paper. It aims to check timing properties and evaluate the scheduling problem in a CPS design. As basis for the proposed evaluation, the design of an Unmanned Aerial Vehicle (UAV) is used. Properties to be evaluated were divided in two categories, one more general (implicit properties) and other tailored for the designed system (explicit properties). Obtained results lead to the conclusion that the use of a single verification technique might not be enough to cover the properties satisfaction in totality, specially in complex CPS.