Applying Integrated Formal Methods on CPS Design

  • Henrique Misson UFSC
  • Fernando Gonçalves IFSC
  • Leandro Buss Becker UFSC


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.

Palavras-chave: Verification, Validation and Test of Systems


E. A. Lee S. A. Seshia Introduction to Embedded Systems - A Cyber-Physical Systems Approach Lee and Seshia 2015.

J. C. Knight "Safety critical systems: challenges and directions" Proceedings of the 24th international conference on software engineering pp. 547-550 2002.

E. Onem A. B. Gurdag M. U. Caglayan "Secure routing in ad hoc networks and model checking?" Proceedings of the First International Conference on Security of Information and Networks pp. 346 2008.

C. Baier J.-P. Katoen Principles of model checking MIT press 2008.

F. Gonçalves "Integrated method for designing complex cyber-physical systems" Ph.D. dissertation 2018.

E. M. Clarke E. A. Emerson "Design and synthesis of synchronization skeletons using branching time temporal logic" Workshop on Logic of Programs pp. 52-71 1981.

A. Pnueli "The temporal logic of programs" 18th Annual Symposium on Foundations of Computer Science (SFCS 1977) pp. 46-57 1977.

L. A. Tuan M. C. Zheng Q. T. Tho "Modeling and verification of safety critical systems: A case study on pacemaker" Secure Software Integration and Reliability Improvement (SSIRI) 2010 Fourth International Conference on pp. 23-32 2010.

M. Leucker C. Schallhart "A brief account of runtime verification" The Journal of Logic and Algebraic Programming vol. 78 no. 5 pp. 293-303 2009.

F. S. Gonçalves G. V. Raffo L. B. Becker "Managing cps complexity: Design method for unmanned aerial vehicles" IFAC-PapersOnLine vol. 49 no. 32 pp. 141-146 2016.

F. S. Gonçalves D. Pereira E. Tovar L. B. Becker "Formal verification of aadl models using uppaal" 2017 VII Brazilian Symposium on Computing Systems Engineering (SBESC) pp. 117-124 2017.

H. Xu P. Wang "Real-time reliability verification for uav flight control system supporting airworthiness certification" PloS one vol. 11 no. 12 pp. e0167168 2016.

L. C. Chaves et al. "Formal verification applied to attitude control software of unmanned aerial vehicles" 2018.

G. Sirigineedi A. Tsourdos B. A. White R. Zbikowski "Modelling and verification of multiple uav mission using smv" 2010.

L. R. Humphrey "Model checking for verification in uav cooperative control applications" in Recent Advances in Research on Unmanned Aerial Vehicles Springer pp. 69-117 2013.

J. Schumann P. Moosbrugger K. Y. Rozier "R2u2: monitoring and diagnosis of security threats for unmanned aerial systems" in Runtime Verification Springer pp. 233-249 2015.

G. Behrmann A. David K. G. Larsen Sfm-rt 2004 Berlin Heidelberg:Springer Berlin Heidelberg pp. 200-236 2004.

R. Barry "Mastering the freertos real time kernel" A Hands-On Tutorial Guide Real Time Engineers Ltd 2016.

A. V. Lara I. B. P. Nascimento J. Arias-Garcia L. B. Becker G. Raffo "Hardware-in-the-loop simulation environment for testing of tilt-rotor uav’s control strategies" 2018.

L. Becker J. Farines J. Bodeveix M. Filali F. Vernadat "Development process for critical embedded systems" in WSE 2010 Gramado. Anais Porto Alegre:SBC pp. 95-108 2010.

Y. Falcone S. Krstić G. Reger D. Traytel "A taxonomy for classifying runtime verification tools" International Conference on Runtime Verification pp. 241-262 2018.

A. d. M. Pedro "Dynamic contracts for verification and enforcement of real-time systems properties" 2018.
MISSON, Henrique; GONÇALVES, Fernando ; BECKER, Leandro Buss. Applying Integrated Formal Methods on CPS Design. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SISTEMAS COMPUTACIONAIS (SBESC), 9. , 2019, Natal. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2019 . p. 137-144. ISSN 2237-5430.