@inproceedings{8101258, author = {Aravantinos, Vincent and Kanav, Sudeep}, title = {Tool Support for Live Formal Verification}, booktitle = {2017 ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS)}, pages = {145-155}, year = {2017}, abstract = {Despite an increasing interest from industry (e.g., DO333 standard [1]), formal verification is still not widely used in production for safety critical systems. This has been recognized for a while and various causes have been identified, one of them being the lack for scalable and cost effective tools. Many such tools exist for formal verification, but few of them are userfriendly: using formal verification generally still requires such an effort that the time spent on the tool prevents the integration of the method in an industrial setting. This paper presents a tool prototype aiming at supporting non-experts in using formal verification. The tooling approach is meant to be cost effective and change-supportive: user-friendliness is designed not only for the non-expert, but also to require minimum effort so that formal verification is triggered even for the non-enthusiast who is not willing to push a button. To do so, we trigger, in a background task, pre-defined formal verification checks at (almost) every change of the model. We only display error messages in case of problem: the user is not disturbed if no problem is detected. To prevent checks to be triggered all the time, we decide to consider only local analyses (i.e., only checks which do not require knowledge of elements in a remote position in the model). This restricts the sort of formal verification that we support, but this is a conscious choice: our motto is ”Let us first make basic techniques very user-friendly; more powerful ones will be considered only when at least the basic techniques have proven to be accepted”.}, doi = {10.1109/MODELS.2017.6}, keywords = {program verification, software tools, formal verification, safety critical systems, automata, component architectures, AutoFOCUS3, formal verification, model-based systems engineering, MbSE}, } @inproceedings{, author = {Mou, Dongyue and Ratiu, Daniel}, title = {Binding requirements and component architecture by using model-based test-driven development}, booktitle = {2012 First IEEE International Workshop on the Twin Peaks of Requirements and Architecture (TwinPeaks)}, pages = {27--30}, year = {2012}, month = sep, abstract = {Model-based testing is a well known technique to generate automatically highly qualitative tests for a given system based on a simplified testing model. Test-driven development is an established development practice in the agile development projects, which implies firstly the partial specification of a system by using tests, and after this, the development of the system. In test driven development the system implementation is continuously checked against the tests in order to assess its correctness with respect to the specification. In this paper we investigate how can these two methods be combined such that the advantages of these two approaches can be leveraged: highly qualitative test-cases used as specification of requirements and support of a continuous checking of architecture. We propose to formalize sub-sets of requirements into models that are amenable to generate tests by using automatic techniques well-known from model based testing. These tests can then be used to check the system architecture specification against the requirements in a continuous manner.}, doi = {10.1109/TwinPeaks.2012.6344557}, keywords = {automatic programming, formal specification, object-oriented programming, program testing, program verification, software architecture, software prototyping, AutoFOCUS3, MIRA, model-based requirements engineering, model-based systems engineering, MbSE}, }