Informatik-Kolloqium Di, 13.07.2010, 16 Uhr
Prof. Peter Ölveczky, University of Oslo
Raum 151, 16:15h
Peter Ölveczky, University of Oslo
Formal Specification and Analysis of Real-Time Systems in Real-Time Maude
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 temporal
logic model checking. Our tool is particularly suitable to specify
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 in advanced
state-of-the-art applications, including scheduling and wireless
sensor network algorithms, communication protocols,
and in finding several bugs in embedded car software that were not
found by standard model checking tools employed in industry.
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 MOMENT2. Real-Time Maude thereby
provides formal model checking capabilities for such languages.
This talk gives a high-level overview of Real-Time Maude and some of
its applications.