Scenario-based Design of Mechatronic Systems
University of Paderborn
Software Engineering Group
DEI - Seminar room
March 25th, 2011
The advanced functions of mechatronic systems today are essentially realized by software that controls complex processes and enables the interaction of multiple system components. For the design of the software in mechatronic systems, we use Modal Sequence Diagrams (MSDs, by Harel and Maoz), a formal interpretation of UML Sequence Diagrams. While MSDs are an intuitive formalism to describe interactions that may, must, or must not happen in a system, inconsistencies are easily introduced in MSD specifications. This talk presents two novel methods for finding inconsistencies in MSD specifications. The first is a novel synthesis approach that effectively finds inconsistencies in timed and untimed MSD specifications by encoding the problem of deciding the realizability of an MSD specification into a two-player game solvable by UPPAAL TIGA. The second method is the simulation of the scenario-based specification based on an improved play-out algorithm (originally by Harel and Marelly). The novelty is that the play-out of an MSD specification can be guided by controllers that could be successfully synthesized for parts of the specification by the aforementioned method. This helps the simulation to avoid avoidable violation (false negatives) that may occur during the play-out of early, under-specified specifications, thus supporting the engineer in more effectively finding inconsistencies in comprehensive specifications of large and possibly dynamic systems.
Advanced software architectures and methodologies