Software Requirements Engineering

Scenario-based, Formal requirements Specification

  • Requirements for cooperating, technical systems (embedded, mechatronic, and cyber-physical systems ..)
  • Requirements for message-based communication behavior
  • Inherent system complexity requires separate consideration of individual application scenarios
  • UML-compliant version of Live Sequence Charts
  • Formal semantics and modal semantics
  • Intuitive requirements modeling structured by use cases
  • Continuous real-time model based on clock zones

Analysis Techniques

  • Simulative validation using Play-out algorithm
  • Reproduce overall behavior, which results from each scenario
  • Automatic synthesis of state-based controllers from MSDs
  • Requirements are consistent and imlementable when a controller can be synthesized from MSDs
  • Synthesis of a counterexample in the case of inconsistencies

Software Modeling

Coordination Realized by Communication

  • Coordination role
  • Behavior
  • Quality of Service

Structure

  • In- and Outgoing Messages
  • In- and Outgoing Signals
  • Horizontal composition
  • Vertical composition
  • Flexible cardinalities
  • Type Save connections

Behavior

  • Refinement of protocol behavior
  • Automatic transformation of role behavior to port behavior
  • Manual refinement
  • Automatic refinement checks
  • Real-Time Statecharts
  • Composition of port behavior
  • Setting and getting of signal values
  • Formal semantics
  • Formal action language

Formal Verification

Domain Specific Formal Requirements Specification with MechatronicUML Timed Computation Tree Logic (MTCTL)

  • Code completion
  • Live syntax check
  • Useful error messages
  • A deadlock shall never appear.
  • All states / transitions are reachable.
  • All messages may arrive at their buffer.
  • ...
  • Complete English sentences rather than complex expressions.
  • Improves understandability
  • Enables requirements experts to understand the properties

Domain-Specific Model Checking Using the Uppaal Model Checker

  • Multi-step semantics-preserving transformations
  • Translation of hierarchical state machines into flat timed automata
  • Translation of domain-specific verification properties
  • Automatic mapping of connectors, message buffers, and QoS properties
  • Understandable domain-specific traces
  • Display of clock values ​​and variable values
  • Display the state of the message buffer and the connector

Model-in-the-Loop Simulation with COTS-Tools

MATLAB Simulink / Stateflow

  • Simulation in Simulink
  • Automatic generation of the network layer
  • Transformation of the state-based behavior to Stateflow

Modelica in Dymola

  • StateGraph2 Extension
  • Free Modelica Licence
  • Asynchronous messages and message buffers
  • Advanced Timing Behavior
  • Modelica Library Award (2012)
  • Layouting based on Graphviz
  • Transformation to StateGraph2 and Real-Time Coordination library elements

Modeling Hardware

Hardware Resources

  • Composition of atomic resources
  • Memory and processors
  • Network protocols
  • Physical Communication Interfaces

Hardware Platform

  • Composition of existing ECUs
  • Composition of platforms
  • Reuse
  • Point -to-point networks
  • Communication buses

Deployment

Design-Space Exploration

  • OCL-based
  • Direct Model Access
  • Integration of reusable libraries
  • Flexible evaluation context
  • Individual query execution
  • Transformation to a model of linear equations(ILP)
  • Alternative Solver
  • LPSolve
  • OPT4J

Code-Generierung

  • Components
  • Real-Time Statecharts
  • Access from the model to native software libraries
  • Container
  • Lifecycle Handline
  • DDS Middleware Adapter
  • Actuator access / sensor access
  • Arduino (.ino)
  • ANSI C99 for x64 and x86 (.c + makefile)
  • nxtOSEK for Lego Mindstorms (.oil + c + makefile)

Reconfiguration

Reconfigurable Components

Reconfiguration Behavior

  • Formal specification
  • Atomicity
  • Consistency
  • Isolation