Dies sind die archivierten Webseiten des Lehrstuhls für Programmierung und Softwaretechnik (PST).
Die Seiten des Software and Computational Systems Lab (SoSy) finden Sie auf https://www.sosy-lab.org/.

Informatik-Kolloqium Di, 13.07.2010, 16 Uhr

— abgelegt unter:

Prof. Peter Ölveczky, University of Oslo

Was
  • Kolloquium
Wann 13.07.2010
von 16:15 bis 19:45
Termin übernehmen vCal
iCal

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.