Validation of Critical Systems with Rewriting Logic in Maude

Critical systems have certain characteristics that, in case of failure, may affect the 'raison d’être' of the system or its environment. The so called cyber-physical system, ubiquitous now a days, that have Internet of Things systems as a subclass, are classified as critical given the characteristics that define them: concurrency, reactivity, synchronism, real-time and high-interaction with the real-world. In this tutorial, presented during II Escola de Informática Teórica e Métodos Formais, Nov. 27 and 28 2017, Recife, PE, Brasil, satellite event to SBMF, we explore the problem of validation of two of these characteristics, namely concurrency and real-time. Our approach relies on Rewriting Logic as underlying logic, implemented on the Maude system where rewritings are identified with deductions in the logic. Simulations can be performed by means of rewriting and state-space search, both in explicit state and symbolic state, and validation by means of model checking, also explicit state and symbolic state. Real-time verification is done on the Real-Time Maude system.

• Slides
• mutex.maude
• mutex-narrow.maude
• 2-reservoir.rtmaude
• k-reservoir.rtmaude