Im Top-Journal IEEE Transactions on Software Engineering (TSE) erscheint ein Artikel von uns über einen neuen Verifikations-Ansatz (DOI: 10.1109/TSE.2021.3110191). Dieser zeichnet sich durch folgendes aus:
- Modellierung von Objekten im physikalischen Modell durch Object Life Cycles
- Verknüpfung von Object Life Cycles mit Activity-Diagrammen anhand von Semantic Action Specifications
- Automatisierte Überführung dieser Modelle in den Code des Tools nuXmv für Model Checking mit Model-driven Transformation
- Allgemeine formale Kriterien für Consistency in Time Logic
Workflow des neuen Verifikations-Ansatzes
