Zustand/Ereignis-basierte Methoden der Softwarespezifikation und -analyse

Dies ist ein Seminar bzw. Hauptseminar. Sowohl Bachelor- als auch Masterstudent(inn)en sind eingeladen, sich zu bewerben.

Conventionally, software systems are formally modelled following either a state-based or an event-based paradigm. For the former, a system is described referring to states and their properties while for the latter it is characterised by events that let the system transition from one state to the next. Both perspectives are essentially equivalent.

During software development, however, the adequacy of state- or event-based methods may change because, for example, in the design phase a functional and thus event-based view appears more natural while in the implementation and verification phase a state-based view prevails. Ideally, it should be possible to employ both paradigms in the design and evaluation of a software system, without having to choose between them.

There are, indeed, specification and verification methods supporting the equal consideration of states and events. With the advancement of model-based development techniques in industry that allow both states and events to be modelled—with Statechart-like notations, for example—these approaches are gaining practical importance.

In this seminar we will review and discuss seminal works on state/event-based formalisms as well as interesting recent innovations, demonstrating their application to a small example system.

• Selecting a pertinent approach from the literature and writing an essay on it, including an application example (5000-6000 words)
• In the final workshop, giving a presentation on your subject (30 mins)

Grading: 65% essay, 35% presentation

Regular attendance as well as observance of deadlines are mandatory.

• Completed undergraduate studies
• Experience with/interest in
  • Formal software specification
  • Software verification
• Self-reliant, focussed working attitude
• Fluent German and/or English, both oral and in writing

Depending on your chosen topic, previous experience may be helpful, but it is not unconditionally required. Please state relevant previous experience upon registration (for example, completed university courses, internships etc).

The number of participants is limited to eight.

We give an introduction to the overall topic on the first appointment. Students select/be provided with single topics from a range of literature, which have to be worked on within specified time periods.

After the orientation phase you hand in an outline of your essay, including a self-researched literature list (3-5 items, in addition to the source proposed by us). Alternatively, participants may give back their topic without this being counted as a failed attempt. The tutor registers participants with the ZPA.

Presentations will be held in a block appointment near the end of the term.

Links connect to the first page of the corresponding article.

• Badouel, Darondeau, Petrucci (2008). Modular synthesis of Petri nets from regular languages.
• Bernardi, Donatelli, Merseguer (2002). From UML sequence diagrams and statecharts to analysable Petri net models.
• Chaki, Clarke, Ouaknine, Sharygina, Sinha (2004). State/event-based software model checking.
• Fraikin, Frappier, Laleau (2005). State-based versus event-based specifications for information systems - a comparison of B and EB.
• Hanisch, Thieme, Lüder, Wienhold (1997). Modeling of PLC behavior by means of timed Net Condition/Event systems.
• Kindler, Vesper (1998). ESTL: a temporal logic for events and states.
• Lavagno, Moon, Brayton, Sangiovanni-Vincentelli (1995). An efficient heuristic procedure for solving the state assignment problem for event-based specifications.
• Salamah, Gates, Kreinovich (2012). Validated templates for specification of complex LTL formulas.
• Shukert (2005). Application of state-event-action logic for controlling complex industrial systems.
• ter Beek, Fantechi, Gnesi, Mazzanti (2011). A state/event-based model-checking approach for the analysis of abstract system properties.

2317

Kick-off meeting: Thursday 17 October 2013, 17:15-18:45 hrs

Workshop: Friday 7 March 2014, 14:00-18:00

Marc Förster, M.Sc.

Seminar (4 ECTS)

Campus: [TBA]
L2P: https://www2.elearning.rwth-aachen.de/ws13/13ws-40227/

• Organisation: Deutsch/English
• Essay, presentation: Deutsch/English.

Most computer science literature is in English, therefore, participants should have a good command of the English language. Essays and presentations can be in either language.

Registration is via the seminar registration website of RWTH Informatik. Please state previous experience, if applicable.

In case of questions, contact Marc Förster, M.Sc.