VECS is an Eclipse-based specification framework for the analysis of software-intensive systems. It includes an implementation of the SAML language and model transformations to verification engines like NuSMV and PRISM. Currently, connectors to high-level Software Engineering tools (like Rhapsody or Enterprise Architect) are being developed.
Publikationen
2014
Lipaczewski, Michael; Filax, Marco; Ortmeier, Frank
Bringing VECS to the World - Challenges and Accomplishments in Teaching of Formal Model Analysis Konferenzbeitrag
In: European Conference on Software Engineering Education. - Herzogenrath : Shaker, S. 217-228, 2014.
@inproceedings{FODB:80901605,
title = {Bringing VECS to the World - Challenges and Accomplishments in Teaching of Formal Model Analysis},
author = { Michael Lipaczewski and Marco Filax and Frank Ortmeier},
url = {https://doi.org/10.2370/9783844030679},
year = {2014},
date = {2014-01-01},
booktitle = {European Conference on Software Engineering Education. - Herzogenrath : Shaker},
pages = {217-228},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Filax, Marco; Gonschorek, Tim; Lipaczewski, Michael; Ortmeier, Frank
On Traceability of Informal Specifications for Model-Based Verification Konferenzbeitrag
In: IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment., S. 11-18, Magdeburg : Univ., 2014.
@inproceedings{FODB:80901202,
title = {On Traceability of Informal Specifications for Model-Based Verification},
author = { Marco Filax and Tim Gonschorek and Michael Lipaczewski and Frank Ortmeier},
url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/07/filax_IMBSA_2014.pdf},
year = {2014},
date = {2014-01-01},
booktitle = {IMBSA 2014: short \& tutorial proceedings of the 4th international symposium on model based safety assessment.},
pages = {11-18},
publisher = {Magdeburg : Univ.},
abstract = {Safety critical systems are often specified by a set of informal requirements. The fulfillment of those requirements has, in general, to be verified through external assessors. In most cases models (i.e. UML diagrams) are used to communicate system architectures and decide whether a given system meets its requirements. Even though, there already exist multiple approaches to verify safety critical systems and assessors would benefit from the usage of model-based system verifications, they are not commonly used in industry. We propose a traceable modeling approach for verifying safety critical systems specified with a set of informal unstructured requirements. The proposed process is divided into three phases: the analysis of the given set of informal requirements, semi-formalization and formalization.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Safety critical systems are often specified by a set of informal requirements. The fulfillment of those requirements has, in general, to be verified through external assessors. In most cases models (i.e. UML diagrams) are used to communicate system architectures and decide whether a given system meets its requirements. Even though, there already exist multiple approaches to verify safety critical systems and assessors would benefit from the usage of model-based system verifications, they are not commonly used in industry. We propose a traceable modeling approach for verifying safety critical systems specified with a set of informal unstructured requirements. The proposed process is divided into three phases: the analysis of the given set of informal requirements, semi-formalization and formalization.
Gonschorek, Tim; Filax, Marco; Lipaczewski, Michael; Ortmeier, Frank
VECS - Verification Enviroment for Critical Systems - Tool Supported Formal Modeling an Verification Buchkapitel
In: IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ., S. 63-64, 2014.
@inbook{FODB:80901373,
title = {VECS - Verification Enviroment for Critical Systems - Tool Supported Formal Modeling an Verification},
author = { Tim Gonschorek and Marco Filax and Michael Lipaczewski and Frank Ortmeier},
url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/07/gonshorek_VECS_2014.pdf},
year = {2014},
date = {2014-01-01},
booktitle = {IMBSA 2014: short \& tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ.},
pages = {63-64},
keywords = {},
pubstate = {published},
tppubtype = {inbook}
}
Nykolaichuk, Mykhaylo; Lipaczewski, Michael; Liebusch, Tino; Ortmeier, Frank
On Efficiently Specifying Models for Model Checking Konferenzbeitrag
In: Proceedings of 4th International Symposium on Model Based Safety and Assessment (IMBSA 2014), 2014.
@inproceedings{nykolaychukIMBSA_2014,
title = {On Efficiently Specifying Models for Model Checking},
author = { Mykhaylo Nykolaichuk and Michael Lipaczewski and Tino Liebusch and Frank Ortmeier},
url = {http://link.springer.com/chapter/10.1007/978-3-319-12214-4_2
https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Nykolaychuk_IMBSA_2014.pdf
},
year = {2014},
date = {2014-01-01},
booktitle = {Proceedings of 4th International Symposium on Model Based Safety and Assessment (IMBSA 2014)},
abstract = {Using formal methods for quality assurance is recommended in many standards for safety critical applications. In most industrial contexts, model checking is the only viable option for formal verification, as interactive approaches often require very highly specialized experts. However, model checking typically suffers from the well-known state-space explosion problem. Due to this problem, engineers typically have to decide on a trade-off between readability and completeness of the model on one side, and the state space size, and thus, computational feasibility on the other. In this paper, we propose a method for reducing the state space by restructuring models. The core idea is to introduce as few additional states as possible by model design making state transitions more complex. To avoid unreadability and infeasible model sizes, we introduce a concept for hierarchical boolean formulas to efficiently specify state transitions. For evaluation purposes, we applied this approach to a case study using the VECS toolkit. In this exemplary case study, we were able to reduce the state space size significantly and make verification time feasible.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Using formal methods for quality assurance is recommended in many standards for safety critical applications. In most industrial contexts, model checking is the only viable option for formal verification, as interactive approaches often require very highly specialized experts. However, model checking typically suffers from the well-known state-space explosion problem. Due to this problem, engineers typically have to decide on a trade-off between readability and completeness of the model on one side, and the state space size, and thus, computational feasibility on the other. In this paper, we propose a method for reducing the state space by restructuring models. The core idea is to introduce as few additional states as possible by model design making state transitions more complex. To avoid unreadability and infeasible model sizes, we introduce a concept for hierarchical boolean formulas to efficiently specify state transitions. For evaluation purposes, we applied this approach to a case study using the VECS toolkit. In this exemplary case study, we were able to reduce the state space size significantly and make verification time feasible.
Heumüller, Robert; Lipaczewski, Michael; Ortmeier, Frank
A Dataflow Notation for SAML - Formal Modeling Without Fearing Timing Constraints Konferenzbeitrag
In: IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ., S. 43-50, 2014.
@inproceedings{FODB:80901349,
title = {A Dataflow Notation for SAML - Formal Modeling Without Fearing Timing Constraints},
author = { Robert Heum\"{u}ller and Michael Lipaczewski and Frank Ortmeier},
year = {2014},
date = {2014-01-01},
booktitle = {IMBSA 2014: short \& tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ.},
pages = {43-50},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
2013
Ortmeier, Frank; Lipaczewski, Michael
Teaching and Training Formal Methods for Safety Critical Systems Konferenz
Proceedings of the 39th Euromicro Conference on Iv Software Engineering and Advanced Applications (SEAA 2013), 2013.
@conference{teaching-saml_SEAA2013,
title = {Teaching and Training Formal Methods for Safety Critical Systems},
author = { Frank Ortmeier and Michael Lipaczewski},
url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Teaching_and_Training_Formal_Methods_for_Safety_Critical-_ystems.pdf},
year = {2013},
date = {2013-01-01},
booktitle = {Proceedings of the 39th Euromicro Conference on Iv Software Engineering and Advanced Applications (SEAA 2013)},
abstract = {Embedded systems become a major part in many domains. This also involves systems which might create heavy damages and injuries when they fail. However, because of the rising number of software components used within this embedded hardware, safety-related problems are hard to discover, and it is even harder to prove that there are none. One approach to guarantee the correctness of a system is model-based safety analysis. They rely on an abstract representation of the system which can then be analyzed using model checkers. The results of these analysis are in general much more precise and often reveal surprising results of failure combinations, where no one had ever thought about before. Nevertheless model-based safety analysis is not used widely. Mainly because it is not well-known and hard to apply to current safety standards which rely on manual approaches. Another fact might be, that most approaches are scientific and in most cases prototypes that are hard to use. In this paper we present some ideas and first steps towards an easy to learn and easy to use model based safety approach. Additionally we present different user-interfaces that are supposed to support the user in his learning.},
keywords = {},
pubstate = {published},
tppubtype = {conference}
}
Embedded systems become a major part in many domains. This also involves systems which might create heavy damages and injuries when they fail. However, because of the rising number of software components used within this embedded hardware, safety-related problems are hard to discover, and it is even harder to prove that there are none. One approach to guarantee the correctness of a system is model-based safety analysis. They rely on an abstract representation of the system which can then be analyzed using model checkers. The results of these analysis are in general much more precise and often reveal surprising results of failure combinations, where no one had ever thought about before. Nevertheless model-based safety analysis is not used widely. Mainly because it is not well-known and hard to apply to current safety standards which rely on manual approaches. Another fact might be, that most approaches are scientific and in most cases prototypes that are hard to use. In this paper we present some ideas and first steps towards an easy to learn and easy to use model based safety approach. Additionally we present different user-interfaces that are supposed to support the user in his learning.
2012
Ortmeier, Frank; Struck, Simon; Lipaczewski, Michael
Using Model-Based Analysis in Certification of Critical Software-Intensive Systems Konferenzbeitrag
In: Softwareengineering 2012 Workshopband, 2012, ISBN: 978-3-88579-293-2.
@inproceedings{se2012-certification,
title = {Using Model-Based Analysis in Certification of Critical Software-Intensive Systems},
author = { Frank Ortmeier and Simon Struck and Michael Lipaczewski},
url = {https://subs.emis.de/LNI/Proceedings/Proceedings199/155.pdf},
isbn = {978-3-88579-293-2},
year = {2012},
date = {2012-02-01},
booktitle = {Softwareengineering 2012 Workshopband},
number = {199},
series = {GI-Edition-Lecture Notes in Informatics (LNI)},
abstract = {Software is taking over more and more functionality in most technical systems, which leads to the term software-intensive or cyber-physical systems. Although this offers many exciting new opportunities, it also makes precise analysis of safety and reliability goals much more complicated. Well-known traditional techniques often reach their limits. Model-based approaches on the other hand can be useful for solving some of these problems. However, in industrial practice answering the question alone is often not sufficient. It is also necessary to explain how answers were found. In this paper, we will show some of the capabilities of modern model-based analysis methods and highlight how they possibly could be used in safety engineering resp. what obstacles need to be avoided.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Software is taking over more and more functionality in most technical systems, which leads to the term software-intensive or cyber-physical systems. Although this offers many exciting new opportunities, it also makes precise analysis of safety and reliability goals much more complicated. Well-known traditional techniques often reach their limits. Model-based approaches on the other hand can be useful for solving some of these problems. However, in industrial practice answering the question alone is often not sufficient. It is also necessary to explain how answers were found. In this paper, we will show some of the capabilities of modern model-based analysis methods and highlight how they possibly could be used in safety engineering resp. what obstacles need to be avoided.
Struck, Simon; Güdemann, Matthias; Lipaczewski, Michael; Ortmeier, Frank
Multi-Objective Optimization of Formal Specifications Konferenz
IEEE 14th International Symposium on High-Assurance Systems Engineering (HASE 2012), 2012.
@conference{Opti-HASE2012,
title = {Multi-Objective Optimization of Formal Specifications},
author = { Simon Struck and Matthias G\"{u}demann and Michael Lipaczewski and Frank Ortmeier},
url = {https://hal.inria.fr/hal-00735640/document},
year = {2012},
date = {2012-01-01},
booktitle = {IEEE 14th International Symposium on High-Assurance Systems Engineering (HASE 2012)},
abstract = {Even in the domain of safety critical systems, safety and reliability are not the only goals and a developing engineer is faced with the problem to find good compromises wrt. other antagonistic objectives, in particular economic aspects of a system. Thus there does not exist a single optimal design variant of a system but only compromises each ``best'' in its own rights . With the rising complexity, especially of cyber-physical systems, the process of manually finding best compromises becomes even more difficult. To cope with this problem, we propose a model-based optimization approach which uses quantitative model-based safety analysis. While the general approach is tool-independent, we implement it technically by introducing well defined variation points to a formal system model. These allow enough variability to cover whole families of systems while still being rigorous enough for formal analysis. From the specification of this family of system variants and a set of objective functions, we compute Pareto optimal sets, which represent best compromises. In this paper we present a framework which allows for optimization of arbitrary quantitative goal functions, in particular probabilistic temporal logic properties used for model-based safety analysis. Nevertheless, the approach itself is well applicable to other domains.},
keywords = {},
pubstate = {published},
tppubtype = {conference}
}
Even in the domain of safety critical systems, safety and reliability are not the only goals and a developing engineer is faced with the problem to find good compromises wrt. other antagonistic objectives, in particular economic aspects of a system. Thus there does not exist a single optimal design variant of a system but only compromises each ``best'' in its own rights . With the rising complexity, especially of cyber-physical systems, the process of manually finding best compromises becomes even more difficult. To cope with this problem, we propose a model-based optimization approach which uses quantitative model-based safety analysis. While the general approach is tool-independent, we implement it technically by introducing well defined variation points to a formal system model. These allow enough variability to cover whole families of systems while still being rigorous enough for formal analysis. From the specification of this family of system variants and a set of objective functions, we compute Pareto optimal sets, which represent best compromises. In this paper we present a framework which allows for optimization of arbitrary quantitative goal functions, in particular probabilistic temporal logic properties used for model-based safety analysis. Nevertheless, the approach itself is well applicable to other domains.
Lipaczewski, Michael; Struck, Simon; Ortmeier, Frank
SAML goes Eclipse - Combining Model-Based Safety Analysis and High-Level Editor Support Konferenz
Proceedings of the 2nd International Workshop on Developing Tools as Plug-Ins (TOPI), IEEE, 2012.
@conference{saml-sde-ICSE2012,
title = {SAML goes Eclipse - Combining Model-Based Safety Analysis and High-Level Editor Support},
author = { Michael Lipaczewski and Simon Struck and Frank Ortmeier},
url = {https://www.researchgate.net/profile/Frank_Ortmeier/publication/261095247_SAML_goes_eclipse_-_Combining_model-based_safety_analysis_and_high-level_editor_support/links/5704fb7408ae13eb88b937cb.pdf},
year = {2012},
date = {2012-01-01},
booktitle = {Proceedings of the 2nd International Workshop on Developing Tools as Plug-Ins (TOPI)},
pages = {67-72},
publisher = {IEEE},
abstract = {Software-intensive systems become more and more important in safety critical applications, mainly because of the rising number and complexity of embedded system. Many traditional safety analysis techniques where developeddecades ago and thus cannot cope with the complexity of modern systems. Model based analysis techniques where developed to deal with the complexity of software-intensive systems. However, due to the lack of tool support these techniques are currently limited to highly skilled experts. Thus model-based analysis is rarely used by system engineers. Based on the safety analysis modeling language (SAML) framework we propose the S3E , which integrates a complete safety analysis environment into the eclipse platform. S3E covers the whole safety analysis work flow. This implies a powerful editor for model creation, a seamless integration of model-analysis tools and presentation as well as evaluation of the analysis results into one environment. In this paper we present the current state of S3E and first experiences with the eclipse plug-in development.},
keywords = {},
pubstate = {published},
tppubtype = {conference}
}
Software-intensive systems become more and more important in safety critical applications, mainly because of the rising number and complexity of embedded system. Many traditional safety analysis techniques where developeddecades ago and thus cannot cope with the complexity of modern systems. Model based analysis techniques where developed to deal with the complexity of software-intensive systems. However, due to the lack of tool support these techniques are currently limited to highly skilled experts. Thus model-based analysis is rarely used by system engineers. Based on the safety analysis modeling language (SAML) framework we propose the S3E , which integrates a complete safety analysis environment into the eclipse platform. S3E covers the whole safety analysis work flow. This implies a powerful editor for model creation, a seamless integration of model-analysis tools and presentation as well as evaluation of the analysis results into one environment. In this paper we present the current state of S3E and first experiences with the eclipse plug-in development.
Lipaczewski, Michael; Struck, Simon; Ortmeier, Frank
Using Tool-Supported Model Based Safety Analysis - Progress and Experiences in SAML Development Konferenz
IEEE 14th International Symposium on High-Assurance Systems Engineering (HASE 2012), 2012.
@conference{S3E-HASE2012,
title = {Using Tool-Supported Model Based Safety Analysis - Progress and Experiences in SAML Development},
author = { Michael Lipaczewski and Simon Struck and Frank Ortmeier},
url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/11/HAZE2012.pdf},
year = {2012},
date = {2012-01-01},
booktitle = {IEEE 14th International Symposium on High-Assurance Systems Engineering (HASE 2012)},
abstract = {Software controls in technical systems are becoming more and more important and complex. Model based safety analysis can give provably correct and complete results, often in a fully automatic way. These methods can answer both logical and probabilistic questions. In common practice, the needed models must be specified in different input languages of different tools depending on the chosen verification tool for the desired aspect. This is time consuming and error-prone. To cope with this problem we developed the safety analysis modeling language (SAML). In this paper, we present a new tool to intuitively create probabilistic, non-deterministic and deterministic specifications for formal analysis. The goal is to give tool-support during modeling and thus make building a formal model less errorprone. The model is then automatically transformed into the input language of state of the art verification engines. We illustrate the approach on a case-study from nuclear power plant domain.},
keywords = {},
pubstate = {published},
tppubtype = {conference}
}
Software controls in technical systems are becoming more and more important and complex. Model based safety analysis can give provably correct and complete results, often in a fully automatic way. These methods can answer both logical and probabilistic questions. In common practice, the needed models must be specified in different input languages of different tools depending on the chosen verification tool for the desired aspect. This is time consuming and error-prone. To cope with this problem we developed the safety analysis modeling language (SAML). In this paper, we present a new tool to intuitively create probabilistic, non-deterministic and deterministic specifications for formal analysis. The goal is to give tool-support during modeling and thus make building a formal model less errorprone. The model is then automatically transformed into the input language of state of the art verification engines. We illustrate the approach on a case-study from nuclear power plant domain.
Güdemann, Matthias; Lipaczewski, Michael; Struck, Simon; Ortmeier, Frank
Unifying Probabilistic and Traditional Formal Model-Based Analysis Konferenz
Proceedings of 8. Dagstuhl-Workshop on Model-Based Development of Embedded Systems (MBEES), 2012.
@conference{saml-process-MBEES2012,
title = {Unifying Probabilistic and Traditional Formal Model-Based Analysis},
author = { Matthias G\"{u}demann and Michael Lipaczewski and Simon Struck and Frank Ortmeier},
url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/11/MBEES2012.pdf},
year = {2012},
date = {2012-01-01},
booktitle = {Proceedings of 8. Dagstuhl-Workshop on Model-Based Development of Embedded Systems (MBEES)},
abstract = {The increasing complexity of modern software-intensive systems makes their analysis much more difficult. At the same time, more and more of theses systems are used in safety-critical environment. Model based safety analysis can help with this problem by giving provably correct and complete results, very often in a fully automatic way. Today, such methods can cope with logical as well as probabilistic questions. However, very often the models used in many model based approaches must be specified in different input languages depending on the chosen verification tool for the desired aspect, which is time consuming and often error-prone. In this paper, we report on our experiences in designing a tool independent specification language (SAML) for model based safety analysis. This allows to use only one model and analyze it with different methods and different verification engines, while guaranteeing the equivalence of the analyzed models. In particular, we discuss challenges and possible solutions to integrate SAML in the development process of real systems.},
keywords = {},
pubstate = {published},
tppubtype = {conference}
}
The increasing complexity of modern software-intensive systems makes their analysis much more difficult. At the same time, more and more of theses systems are used in safety-critical environment. Model based safety analysis can help with this problem by giving provably correct and complete results, very often in a fully automatic way. Today, such methods can cope with logical as well as probabilistic questions. However, very often the models used in many model based approaches must be specified in different input languages depending on the chosen verification tool for the desired aspect, which is time consuming and often error-prone. In this paper, we report on our experiences in designing a tool independent specification language (SAML) for model based safety analysis. This allows to use only one model and analyze it with different methods and different verification engines, while guaranteeing the equivalence of the analyzed models. In particular, we discuss challenges and possible solutions to integrate SAML in the development process of real systems.
2011
Güdemann, Matthias; Lipaczewski, Michael; Ortmeier, Frank
Tool Supported Model-Based Safety Analysis and Optimization Konferenz
Proceedings of the 17th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC 2011), 2011.
@conference{modelBasedAnalysisToolPRDC2011,
title = {Tool Supported Model-Based Safety Analysis and Optimization},
author = { Matthias G\"{u}demann and Michael Lipaczewski and Frank Ortmeier},
url = {http://ieeexplore.ieee.org/abstract/document/6133100/},
year = {2011},
date = {2011-01-01},
booktitle = {Proceedings of the 17th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC 2011)},
abstract = {Although model-based approaches can yield very precises safety analyses, they are rarely used in practice. The reason is, that most techniques are very difficult to apply and almost always require separate models and tools. In this paper we present an outline for the integration of different model-based safety analysis and safety optimization methods into a single tool framework. We present the envisioned workflow and some of the requirements for the tool integration. Because of its wide acceptance, platform independence and its well-documented API, we chose the Eclipse platform as framework foundation.},
keywords = {},
pubstate = {published},
tppubtype = {conference}
}
Although model-based approaches can yield very precises safety analyses, they are rarely used in practice. The reason is, that most techniques are very difficult to apply and almost always require separate models and tools. In this paper we present an outline for the integration of different model-based safety analysis and safety optimization methods into a single tool framework. We present the envisioned workflow and some of the requirements for the tool integration. Because of its wide acceptance, platform independence and its well-documented API, we chose the Eclipse platform as framework foundation.
VECS