Monday, November 25, 2019 — by Peter Csaba Ölveczky from University of Oslo
Formal Specification and Analysis of Real-Time Systems in Real-Time Maude
Seminar organized by CONVECS (Gwen Salaün) At 16:00 in F107 at INRIA MontbonnotAbstract: Real-Time Maude is a tool that extends the rewriting-logic-based Maude system to support the executable formal modeling and analysis of real-time systems. Real-Time Maude is characterized by its general and expressive, yet intuitive, specification formalism, and offers a spectrum of formal analysis methods, including: rewriting for simulation purposes, search for reachability analysis, and both untimed and metric temporal logic model checking. Real-Time Maude is particularly suitable for specifying real-time systems in an object-oriented style, and its flexible formalism makes it easy to model different forms of communication.
This modeling flexibility, and the usefulness of Real-Time Maude for both simulation and model checking, has been demonstrated on many advanced state-of-the-art applications, including both distributed protocols of different kinds and industrial embedded systems. Furthermore, Real-Time Maude’s expressiveness has also been
exploited for defining the formal semantics of MDE languages for real time/embedded systems, including Ptolemy discrete-event models, a subset of the avionics modeling standard AADL, and a timed extension of the MOMENT2 model transformation framework. Real-Time Maude thereby provides formal model checking capabilities for these languages for free, and such analysis has been integrated into the tool environment of a number of modeling languages.
This talk gives a high-level overview of Real-Time Maude and some of its applications.
This modeling flexibility, and the usefulness of Real-Time Maude for both simulation and model checking, has been demonstrated on many advanced state-of-the-art applications, including both distributed protocols of different kinds and industrial embedded systems. Furthermore, Real-Time Maude’s expressiveness has also been
exploited for defining the formal semantics of MDE languages for real time/embedded systems, including Ptolemy discrete-event models, a subset of the avionics modeling standard AADL, and a timed extension of the MOMENT2 model transformation framework. Real-Time Maude thereby provides formal model checking capabilities for these languages for free, and such analysis has been integrated into the tool environment of a number of modeling languages.
This talk gives a high-level overview of Real-Time Maude and some of its applications.
Bio: Peter Ölveczky received his PhD in computer science from the University of Bergen, Norway, in 2000, having performed his thesis research at SRI International. He was assistant and then associate professor at the University of Oslo 2001-2008, and has been a full professor there since 2008. He was also a post-doctoral researcher at the University of Illinois at Urbana-Champaign (UIUC) 2002-2004, and a visiting researcher at UIUC 2008-2018.
Ölveczky’s research focuses on formal methods, in particular for real-time systems. He is the developer of the Real-Time Maude tool, which has been used to formally model and analyze a large range of advanced systems, including scheduling protocols, distributed data stores, wireless sensor network algorithms, the human thermoregulatory
system, mobile ad hoc networks, avionics systems, human cognitive processes, and so on.
Ölveczky has organized 13 international scientific workshops/conferences, has written one book and edited a number of scientific books and journal issues, and is a member of the steering committees of FACS and SEFM.
Ölveczky’s research focuses on formal methods, in particular for real-time systems. He is the developer of the Real-Time Maude tool, which has been used to formally model and analyze a large range of advanced systems, including scheduling protocols, distributed data stores, wireless sensor network algorithms, the human thermoregulatory
system, mobile ad hoc networks, avionics systems, human cognitive processes, and so on.
Ölveczky has organized 13 international scientific workshops/conferences, has written one book and edited a number of scientific books and journal issues, and is a member of the steering committees of FACS and SEFM.
