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
- Atomicity
- Consistency
- Isolation
