Modeling complex system requirements often requires specifying system components in separate models, which can be validated and verified in isolation from each other, and then integrating all components’ behavior in order to validate the operation of the whole system. If models are executable, as for state-based formal specifications, engines to orchestrate the simulation of separate component operational models are extremely useful. This paper presents an approach for the co-simulation, according to predefined orchestration schemas, of state-based models of separate components of a Discrete Event System. More precisely, we exploit the Abstract State Machine (ASM) formal method as state-based formalism, and we (i) define a set of operators to compose ASMs that communicate with each other through I/O events, and (ii) present an engine to execute the compositional simulation of the ASMs as a whole assembly. As proof of concepts, we use a set of model examples of Discrete Event Systems of increasing complexity to show the application of our approach and to evaluate its effectiveness in co-simulating models of real systems.

Abstract This tutorial paper introduces ASMETA, a comprehensive suite of integrated tools around the formal method Abstract State Machines to specify and analyze the executable behavior of discrete event systems. ASMETA supports the entire system development life-cycle, from the specification of the functional requirements to the implementation of the code, in a systematic and incremental way. This tutorial provides an overview of ASMETA through an illustrative case study, the Pill-Box, related to the design of a smart pillbox device. It illustrates the practical use of the range of modeling and V&V techniques available in ASMETA and C++ code generation from models, to increase the quality and reliability of behavioral system models and source code.

Combinatorial testing is a widely adopted technique for efficiently detecting faults in software. The quality of combinatorial test generators plays a crucial role in achieving effective test coverage. Evaluating combinatorial test generators remains a challenging task that requires diverse and representative benchmarks. Having such benchmarks might help developers to test their tools, and improve their performance. For this reason, in this paper, we present BenCIGen, a highly configurable generator of benchmarks to be used by combinatorial test generators, empowering users to customize the type of benchmarks generated, including constraints and parameters, as well as their complexity. An initial version of such a tool has been used during the CT-Competition, held yearly during the International Workshop on Combinatorial Testing. This paper describes the requirements, the design, the implementation, and the validation of BenCIGen. Tests for the validation of BenCIGen are derived from its requirements by using a combinatorial interaction approach. Moreover, we demonstrate the tool’s ability to generate benchmarks that reflect the characteristics of real software systems. BenCIGen not only facilitates the evaluation of existing generators but also serves as a valuable resource for researchers and practitioners seeking to enhance the quality and effectiveness of combinatorial testing methodologies.

Abstract Modern automotive systems with adaptive control features require rigorous analysis to guarantee correct operation. We report our experience in modeling the automotive case study from the ABZ2020 conference using the ASMETA toolset, based on the Abstract State Machine formal method. We adopted a seamless system engineering method: from an incremental formal specification of high-level requirements to increasingly refined ASMETA models, to the C++ code generation from the model. Along this process, different validation and verification activities were performed. We explored modeling styles and idioms to face the modeling complexity and ensure that the ASMETA models can best capture and reflect specific behavioral patterns. Through this realistic automotive case study, we evaluated the applicability and usability of our formal modeling approach.

This paper proposes an evaluation framework for autonomous systems, called LENS. It is an instrument to make an assessment of a system through the lens of abilities related to adaptation and smartness. The assessment can then help engineers understand in which direction it is worth investing to make their system smarter. It also helps to identify possible improvement directions and to plan for concrete activities. Finally, it helps to make a re-assessment when the improvement has been performed in order to check whether the activity plan has been accomplished.Given the high variability in the various domains in which autonomous systems are and can be used, LENS is defined in abstract terms and instantiated to a specific and important class of medical devices, i.e., Programmable Electronic Medical Systems (PEMS). The instantiation, called LENSPEMS, is validated in terms ofapplicability, i.e., how it is applicable to real PEMS,generalizability, i.e., to what extent LENSPEMSis generalizable to the PEMS class of systems, andusefulness, i.e., how it is useful in making an assessment and identifying possible directions of improvement towards smartness.

Abstract In this paper, we present an approach to conformance testing based on abstract state machines (ASMs) that combines model refinement and test execution (RATE) and its application to three case studies. The RATE approach consists in generating test sequences from ASMs and checking the conformance between code and models in multiple iterations. The process follows these steps: (1) model the system as an abstract state machine; (2) validate and verify the model; (3) generate test sequences automatically from the ASM model; (4) execute the tests over the implementation and compute the code coverage; (5) if the coverage is below the desired threshold, then refine the abstract state machine model to add the uncovered functionalities and return to step 2. We have applied the proposed approach in three case studies: a traffic light control system (TLCS), the IEEE 11073‐20601 personal health device (PHD) protocol, and the mechanical ventilator Milano (MVM). By applying RATE, at each refinement level, we have increased code coverage and identified some faults or conformance errors for all the case studies. The fault detection capability of RATE has also been confirmed by mutation analysis, in which we have highlighted that, many mutants can be killed even by the most abstract models.

Neural networks have been widely applied for performing tasks in critical domains, such as, for example, the medical domain; their robustness is, therefore, important to be guaranteed. In this paper, we propose a robustness definition for neural networks used for regression, by tackling some of the problems of existing robustness definitions. First of all, by following recent works done for classification problems, we propose to define the robustness of networks used for regression w.r.t. alterations of their input data that can happen in reality. Since different alteration levels are not always equally probable, the robustness definition is parameterized with the probability distribution of the alterations. The error done by this type of networks is quantifiable as the difference between the estimated value and the expected value; since not all the errors are equally critical, the robustness definition is also parameterized with a “tolerance” function that specifies how the error is tolerated. The current work has been motivated by the collaboration with the industrial partner that has implemented a medical sensor employing a Multilayer Perceptron for the estimation of the blood oxygen pressure. After having computed the robustness for the case study, we have successfully applied three techniques to improve the network robustness: data augmentation with recombined data, data augmentation with altered data, and incremental learning. All the techniques have proved to contribute to increasing the robustness, though in different ways.

Classification using Artificial Neural Networks (ANNs) is widely applied in critical domains, such as autonomous driving and in the medical practice; therefore, their validation is extremely important. A common approach consists in assessing the network robustness, i.e., its ability to correctly classify input data that is particularly challenging for classification. We recently proposed a robustness definition that considers input data degraded by alterations that may occur in reality; the approach was originally devised for image classification in the medical domain. In this paper, we extend the definition of robustness to any type of input for which some alterations can be defined. Then, we present ROBY, a tool for ROBustness analYsis of ANNs. The tool accepts different types of data (images, sounds, text, etc.) stored either locally or on Google Drive. The user can use some alterations provided by the tool, or define their own. The robustness computation can be performed either locally or remotely on Google Colab. The tool has been experimented for robustness computation of image and sound classifiers, used in the medical and automotive domains.

Modern software systems operate in complex and changing environments and are exposed to multiple sources of uncertainty. Testing methods shall be tailored to uncertainty as a first-class concern in order to quantify it and deliver increased confidence in the level of assurance of the final product. In this paper, we introduce novel model-based exploration strategies that generate test cases targeting uncertain components of the system under test. Our testing framework leverages Markov Decision Processes as modeling formalism of choice. The tester explicitly specifies uncertainty by means of beliefs attached to transition probabilities. The structural properties of the model and the uncertainty specification are then exploited to drive the test case generation process. Bayesian inference is used to achieve this objective by updating the initial beliefs through the evidence collected by testing. The proposed uncertainty-aware test selection strategies have been systematically evaluated on three realistic benchmarks and nine synthetic systems exhibiting up to 10k model transitions. We demonstrate the effectiveness of the novel strategies with well-established metrics. Results show they outperform existing testing methods with a gain up to 2.65× in terms of accuracy of the inference process.

During the COVID-19 pandemic, many researchers all over the world have offered their time and competencies to face the heavy consequences of the disease. This is the case of a group of physicists, engineers, and physicians that around the middle of March 2020 started to develop a simplified mechanical lung ventilator, called MVM (Mechanical Ventilator Milano), to answer the high request of ventilators for Acute Respiratory Distress Syndrome (ARDS) in intensive care units. A prototype was ready in around one month. Since medical software malfunctions can lead to injuries or death of patients, before marketing MVM ventilators and distributing them in hospitals, software certification in accordance with the IEC 62304 standard was mandatory to guarantee system reliability. The team was then complemented by computer scientists specifically devoted to this task. The software re-engineering process, which lasted around two months from the end of the prototype, brought to a strong re-implementation of the device software components, which involved all the stakeholders in a continuous integration setting. In this paper, we report the experience of the MVM control SW re-engineering necessary to show evidence that the SW adheres to the standards and to consequently obtain the certification. We share results and lessons learned from this social project, where more than 100 volunteer researchers worked towards software certification at the extreme of their strength to get a real device finished in a rush since strongly required to support physicians in treating COVID-19 patients.

Abstract According to best practices of model‐driven engineering, the implementation of a system should be obtained from its model through a systematic model‐to‐code transformation. We present in this paper a methodology supported by the Asm2C++ tool, which allows the users to generate C++ code from abstract state machine models. Thanks to Asm2C++, the implementation is generated in a seamless manner with an assurance of potential bug freeness of the generated code. Following the same approach, model‐based testing suggests deriving also (unit) tests from abstract models. We extend the Asm2C++ tool such that it can automatically produce unit tests for the generated code. Abstract test sequences, either generated randomly or through model checking, are translated to concrete C++ unit tests using the Boost library. In a similar manner, also, scenarios are generated in a behavior‐driven development (BDD) approach. To guarantee the correctness of the transformation process, we define a mechanism to test the correctness of the model‐to‐code transformation with respect to two main criteria: syntactical correctness and semantic correctness, which is based on the definition of conformance between the specification and the code. Using this approach, we have devised a process able to test the generated code by reusing unit tests. The process has been used to validate our model‐to‐code transformations.

Summary Nowadays, there exists an increasing demand for reliable software systems able to fulfill their requirements in different operational environments and to cope with uncertainty that can be introduced both at design‐time and at runtime because of the lack of control over third‐party system components and complex interactions among software, hardware infrastructures and physical phenomena. This article addresses the problem of the discrepancy between measured data at runtime and the design‐time formal specification by using aninverse uncertainty quantificationapproach. Namely, we introduce a methodology calledMETRICand its supporting toolchain to quantify and mitigate software system uncertainty during testing by combining (on‐the‐fly)model‐based testingandBayesian inference. Our approach connects probabilistic input/output conformance theory with statistical hypothesis testing in order to assess if the behaviour of the system under test corresponds to its probabilistic formal specification provided in terms of aMarkov decision process. An uncertainty‐aware model‐based test case generation strategy is used as a means to collect evidence from software components affected by sources of uncertainty. Test results serve as input to a Bayesian inference process that updates beliefs on model parameters encoding uncertain quality attributes of the system under test. This article describes our approach from both theoretical and practical perspectives. An extensive empirical evaluation activity has been conducted in order to assess the cost‐effectiveness of our approach. We show that, under same effort constraints, our uncertainty‐aware testing strategy increases the accuracy of the uncertainty quantification process up to 50 times with respect to traditional model‐based testing methods.

Combinatorial interaction testing (CIT) is a useful testing technique to address the interaction of input parameters in software systems. CIT has been used as a systematic technique to sample the enormous test possibilities. Most of the research activities focused on the generation of CIT test suites as a computationally complex problem. Less effort has been paid for the application of CIT. To apply CIT, practitioners must identify the input parameters for the Software‐under‐test (SUT), feed these parameters to the CIT test generation tool, and then run those tests on the application with some pass and fail criteria for verification. Using this approach, CIT is used as a black‐box testing technique without knowing the effect of the internal code. Although useful, practically, not all the parameters having the same impact on the SUT. This paper introduces a different approach to use the CIT as a gray‐box testing technique by considering the internal code structure of the SUT to know the impact of each input parameter and thus use this impact in the test generation stage. The case studies results showed that this approach would help to detect new faults as compared to the equal impact parameter approach.

Summary Regular expressions are used to characterize sets of strings (ie, languages) using a pattern‐based syntax. They are applied in different contexts as, for example, data validation in Web forms. However, writing a regular expression that exactly captures the desired set of strings could be particularly difficult, and techniques are sought to validate regular expressions or test their use in applications. A common means to regular expression validation and testing is the generation of a set of labelled strings (ie, strings together with their evaluation). We here propose a fault‐based approach for generating strings usable as tests for regular expressions. We define some fault classes representing mistakes that could be made when writing a regular expression, and we introduce the notion of distinguishing string, ie, a string that is able to expose a fault. Given a regular expression, our approach generates a test suite composed of distinguishing strings that are able to detect possible faults in the regular expression. We present different versions of the approach, which provide different results in terms of test suite size and generation time. Experiments show that the proposed approach can generate compact test suites and that, using suitable optimizations, the generation time is reasonable. Exploiting the proposed fault classes, we use the notion of mutation score to assess the ability of a generic set of strings in exposing possible faults contained in the regular expression under test. A comparison with other test generation tools in terms of mutation score, size, and generation time shows the advantages and limits of our approach.

Model-based test generation by model checking is a well-known testing technique that, however, suffers from the state explosion problem of model checking and it is, therefore, not always applicable. In this paper, we address this issue by decomposing a system model into suitable subsystem models separately analyzable. Our technique consists in decomposing that portion of a system model that is of interest for a given testing requirement, into a tree of subsystems by exploiting information on model variable dependency. The technique generates tests for the whole system model by merging tests built from those subsystems. We measure and report effectiveness and efficiency of the proposed decomposition-based test generation approach, both in terms of coverage and time.

Modern software systems are required to operate in a highly uncertain and changing environment. They have to control the satisfaction of their requirements at run-time, and possibly adapt and cope with situations that have not been completely addressed at design-time. Software engineering methods and techniques are, more than ever, forced to deal with change and uncertainty (lack of knowledge) explicitly. For tackling the challenge posed by uncertainty in delivering more reliable systems, this paper proposes a novel online Model-based Testing technique that complements classic test case generation based on pseudo-random sampling strategies with an uncertainty-aware sampling strategy. To deal with system uncertainty during testing, the proposed strategy builds on an Inverse Uncertainty Quantification approach that is related to the discrepancy between the measured data at run-time (while the system executes) and a Markov Decision Process model describing the behavior of the system under test. To this purpose, a conformance game approach is adopted in which tests feed a Bayesian inference calibrator that continuously learns from test data to tune the system model and the system itself. A comparative evaluation between the proposed uncertainty-aware sampling policy and classical pseudo-random sampling policies is also presented using the Tele Assistance System running example, showing the differences in achieved accuracy and efficiency.

Abstract The use of formal methods is often recommended to guarantee the provision of necessary services and to assess the correctness of critical properties, such as functional safety, cybersecurity, and reliability, in medical and health care devices. In the past, several formal and rigorous methods have been proposed and consequently applied for trustworthy development of medical software and systems. In this paper, we perform a systematic literature review on the available state of the art in this domain. We collect the relevant literature on the use of formal methods for modeling, design, development, verification, and validation of software‐intensive medical systems. We apply standard systematic literature review techniques and run several queries in well‐known repositories to obtain information that can be useful for people who are either already working in this field or planning to start. Our study covers both quantitative and qualitative aspects of the subject.

NuSMV is a well-known tool for system verification that permits to verify both CTL and LTL properties. Although the tool is very powerful, it offers a minimal support for the editing and validation (e.g., by simulation) of models and of requirements specified as temporal properties. In this paper, we propose NuSeen, a framework that assists a designer during the modeling and V&V activities when using NuSMV. In addition to an editor furnished with syntax highlighting, autocompletion, and outline, NuSeen also provides some tools for visualizing the variable dependencies, and graphically visualizing the counterexamples. It helps the designer in validating the model by checking certain qualities like minimality and completeness. Moreover, the framework also provides facilities for model-based testing by means of a test suite generator that is able to generate tests achieving value and decision coverage for NuSMV models.

Building a feature model for an existing SPL can improve the automatic analysis of the SPL and reduce the effort in maintenance. However, developing a feature model can be error prone, and checking that it correctly identifies each actual product of the SPL may be unfeasible due to the huge number of possible configurations. We apply mutation analysis and propose a method to detect and remove conformance faults by selecting special configurations that distinguish a feature model from its mutants. We propose a technique that, by iterating this process, is able to repair a faulty model. We devise several variations of a simple hill climbing algorithm for automatic fault removal and we compare them by a series of experiments on three different sets of feature models. We find that our technique is able to improve the conformance of around 90% of the models and find the correct model in around 40% of the cases.

We present a novel fault-based approach for testing feature models (FMs). We identify several fault classes that represent possible mistakes one can make during feature modeling. We introduce the concept of distinguishing configuration, i.e., a configuration that is able to detect a given fault. Starting from this definition, we devise a technique, based on the use of a logic solver, able either to find distinguishing configurations to be used as tests or to prove that a mutation produces an equivalent feature model. Compact test suites can be produced by exploiting an SMT solver. The experiments show that our methodology is viable and produces reasonable sized test suites in a short time. W.r.t. the approaches that use only the products, our approach has a better fault detection capability and requires fewer tests.

Self-adaptive systems autonomously adapt their behavior at run-time to react to internal dynamics and to uncertain and changing environment conditions. Specification and verification of self-adaptive systems are generally very difficult to carry out due to their high complexity, especially when involving time constraints. In the last case, in fact, the correctness of systems depends also on the time associated with events. This paper introduces a formal approach to specify and verify the self-adaptive behavior of real-time systems. Our specification formalism is based on Time-Basic Petri nets, a particular timed extension of Petri nets. We propose adaptation models to realize self-adaptation with temporal constraints and we adopt a zone-based modeling approach to support separation of concerns during the modeling phase. Zones identified during the modeling phase can be then used as modules (TB Petri subnets) either in isolation, to verify intra-zone properties, or all together, to verify inter-zone properties over the entire system model and check that all the temporal deadlines are met. We illustrate our approach by modeling and verifying a time-critical Gas Burner system that exhibits a self-healing behavior.

Medical device software malfunctioning can lead to injuries or death for humans and, therefore, its development should adhere to certification standards. However, these standards establish general guidelines on the use of common software engineering activities without any indication regarding methods and techniques to assure safety and reliability. This paper presents a formal development process, based on the Abstract State Machine method, that integrates most of the activities required by the standards. The process permits to obtain, through a sequence of refinements, more detailed models that can be formally validated and verified. Offline and online testing techniques permit to check the conformance of the implementation w.r.t. the specification. The process is applied to the validation of the SAM medical software, that is used to measure the patients' stereoacuity in the diagnosis of amblyopia.

One of the well-known techniques for model-based test generation exploits the capability of model checkers to return counterexamples upon property violations. However, this approach is not always optimal in practice due to the required time and memory, or even not feasible due to the state explosion problem of model checking. A way to mitigate these limitations consists in decomposing a system model into suitable subsystem models separately analyzable. In this paper, we show a technique to decompose a system model into subsystems by exploiting the model variables dependency, and then we propose a test generation approach which builds tests for the single subsystems and combines them later in order to obtain tests for the system as a whole. Such approach mitigates the exponential increase of the test generation time and memory consumption, and, compared with the same model-based test generation technique applied to the whole system, shows to be more efficient. We prove that, although not complete, the approach is sound.

In the context of automatic test generation, the use of propositional satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers is becoming an attractive alternative to traditional algorithmic test generation methods, especially when testing Boolean expressions. The main advantages are the capability to deal with constraints over the inputs, the generation of compact test suites and the support for fault-detecting test generation methods. However, these solvers normally require more time and a greater amount of memory than classical test generation algorithms, making their applicability not always feasible in practice. In this paper, we propose several ways to optimize the SAT/SMT-based process of test generation for Boolean expressions and we compare several solving tools and propositional transformation rules. These optimizations promise to make SAT/SMT-based techniques as efficient as standard methods for testing purposes, especially when dealing with Boolean expressions, as proved by our experiments.

Summary Among validation techniques,model reviewis a static analysis approach that can be performed at the early stages of software development, at the specification level, and aims at determining if a model owns certain quality attributes (like completeness, consistency and minimality). However, the model review capability to detect behavioural faults has never been measured. In this paper, a methodology and a supporting tool for evaluating the fault detection capability of a NuSMV model advisor are presented, which performs an automatic static model review of NuSMV models. The approach is based on the use ofmutationin a similar way as in mutation testing: several mutation operators for NuSMV models are defined, and the model advisor is used to detect behavioural faults by statically analysing mutated specifications. In this way, it is possible to measure the model advisor ability to discover faults. To improve the quality of the analysis, the equivalence between a NuSMV model and any of its mutants must be checked. To perform this task, this paper proposes a technique based on the concept of equivalent Kripke structures, as NuSMV models are Kripke structures. A number of experiments assess the fault‐detecting capability, precision and accuracy of the proposed approach. Analysis of variance is used to check if the results are statistically significant. Some relationships among mutation operators and model quality attributes are also established. Copyright © 2014 John Wiley & Sons, Ltd.

In this paper the CITLAB tool for Combinatorial Interaction Testing is presented. The tool allows importing/exporting models of combinatorial problems from/to different application domains, by means of a common interchange syntax notation and a corresponding interoperable semantic metamodel. Moreover, the tool is a framework allowing embedding and transparent invocation of multiple, different implementations of combinatorial algorithms. CITLAB has been designed tightly integrated with the Eclipse IDE framework, by means of its plug-in extension mechanism. It is intended to easy the spread of CIT testing both in industrial practice and in academic research, by allowing users and researchers to apply multiple test suite generation algorithms, each with its peculiarities, on the same problem models, and let them compare the results in order to select the one that best fits their needs, while alleviating from the pain of knowing all the different details and notations of the underlying CIT tools.

Code coverage is usually used as a measurement of testing quality and as adequacy criterion. Unfortunately, code coverage is very sensitive to modifications of the code structure, and, therefore, we can achieve the same degree of coverage with different testing effort by writing the same program in syntactically different ways. For this reason, code coverage can provide the tester with misleading information. In order to understand how a testing criterion is affected by code structure modifications, we have introduced a way to measure the sensitivity of coverage to code changes by means of code-to-code transformations. However the manual execution of the robustness analysis is tedious, time consuming and error prone. In order to solve these issues we present AURORA, a tool that automates the robustness analysis process and leverages the capabilities offered from several existing tools. AURORA has an extendible architecture that concretely supports the tester in the execution of the robustness analysis. Due to this extendible architecture, each user can personalize the robustness analysis to his/her needs. AURORA allows the user to add new transformations by using TXL, which is a programming language specifically designed to support source transformation tasks. It performs the coverage evaluation by using existing code coverage tools and is based on the use of the JUnit framework.

Although the research community around combinatorial interaction testing has been very active for several years, it has failed to find common solutions on some issues. First of all, there is not a common abstract nor concrete language to express combinatorial problems. Combinatorial testing generator tools are strongly decoupled making difficult their interoperability and the exchange of models and data. In this paper, we propose an abstract and concrete specific language for combinatorial problems. It features and formally defines the concepts of parameters and types, constraints, seeds, and test goals. The language is defined by means of XTEXT, a framework for the definition of domain-specific languages. XTEXT is used to derive a powerful editor integrated with eclipse and with all the expected features of a modern editor. Eclipse is also used to build an extensible framework in which test generators, importers, and exporters can be easily added as plugins.

SUMMARY Combinatorial interaction testing (CIT) is a testing technique that requires covering all t‐sized tuples of values out of n parameter attributes or properties modelled after the input parameters or the configuration domain of a system under test. CIT test suites have shown to be very effective in software testing already at pairwise (t = 2) level, and the effectiveness of CIT grows with the tuple width t. Unfortunately, the number of tuples to be tested also does grow. In order to reduce the testing effort, researchers addressed the issue of computing minimal‐sized CIT test suites with effective and scalable algorithms. However, still very few generally applicable t‐wise covering construction algorithms (and tools) do exist in literature. This paper presents an original greedy algorithm to compute t‐wise covering mixed covering arrays with constant space complexity, irrespective of the number of involved parameters and strength of interaction. The proposed algorithm has been implemented in a prototype tool, featuring also support for user constraints over the inputs. Assessment of the tool performance on a set of large, real‐world test systems is reported, with results encouraging its adoption in industrial production environments. Copyright © 2011 John Wiley & Sons, Ltd.

Recent advances in propositional satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers are increasingly rendering SAT and SMT-based automatic test generation an attractive alternative to traditional algorithmic test generation methods. The use of SAT/SMT solvers is particularly appealing when testing Boolean expressions: These tools are able to deal with constraints over the models, generate compact test suites, and they support fault-based test generation methods. However, these solvers normally require more time and greater amount of memory than classical test generation algorithms, limiting their applicability. In this paper we propose several ways to optimize the process of test generation and we compare several SAT/SMT solvers and propositional transformation rules. These optimizations promise to make SAT/SMT-based techniques as efficient as standard methods for testing purposes, especially when dealing with Boolean expressions, as proved by our experiments.

Abstract This paper presents a model‐driven software process suitable to develop a set of integrated tools around a formal method. This process exploits concepts and technologies of the Model‐driven Engineering (MDE) approach, such as metamodelling and automatic generation of software artifacts from models. We describe the requirements to fulfill and the development steps of this model‐driven process. As a proof‐of‐concept, we apply it to the Finite State Machines and we report our experience in engineering a metamodel‐based language and a toolset for the Abstract State Machine formal method. Copyright © 2011 John Wiley & Sons, Ltd.

In this paper, we present our position and experience on integrating formal methods with the model-driven engineering (MDE) approach to software development. Both these two approaches have advantages and disadvantages, and we here show how the advantages of one can be exploited to cover or weaken the disadvantages of the other. We also propose an in-the-loop integration which allows the development of a general framework for software engineering where rigorousness and preciseness of formal methods are combined with flexibility and automation of the MDE. We discuss the feasibility of unifying these two separate worlds, referring to our experience on integrating the abstract state machine formal method with the Eclipse modeling framework supporting MDE facilities.

Under certain constraints the test case generation problem can be represented as a model checking problem, thus enabling the use of powerful model checking tools to perform the test case generation automatically. There are, however, several different model checking techniques, and to date there is little evidence and comparison on which of these techniques is best suited for test case generation. This paper presents the results of an evaluation of several different model checkers on a set of realistic formal specifications given in the SCR notation. For each specification test cases are generated for a set of coverage criteria with each of the model checkers using different configurations. The evaluation shows that the best suited model checking technique and optimization very much depend on the specification that is used to generate test cases. However, from the experiments we can draw general conclusions about which optimizations are useful and which model checking technique is best suited for which type of model. Finally, we demonstrate that by combining several model checking techniques it is possible to significantly speed up test case generation and also achieve full test coverage for cases where none of the techniques by itself would succeed.

This paper describes a scenario-based methodology for system-level design validation based on the Abstract State Machines formal method. This scenario-based approach complements an existing model-driven design methodology for embedded systems based on the SystemC UML profile. It allows the designer to functionally validate system components from SystemC UML designs early at high levels of abstraction and without requiring strong skills and expertise on formal methods. A validation tool integrated into an existing model-driven co-design environment to support the proposed scenario-based validation flow is also presented.

This paper reports our experience in exploiting the metamodelling approach of model-driven language engineering to define a standard modelling language for the Abstract State Machines (ASMs) formal method, and develop a general framework (ASMETA) for a wide interoperability of ASM tools in a model-driven development context. We describe the requirements to fulfill and the design, implementation, validation, and tools development steps necessary to support such a language engineering life cycle. We finally discuss the benefits/limits of a model-driven language engineering approach with respect to traditional techniques primarily used for the same goal.

We present a temporal framework suitable for the specification and verification of safety properties of real time hybrid systems. We show that, given suitable assumptions (like non-Zenoness and left continuity) continuous time can be discretized by introducing a next operator that is similar to the one usually found in discrete time temporal logics and can be safely and effectively used in specifications as well as in verification. The proofs of properties can be conducted in a deductive style, and can be easily automated, especially when they are based on induction. We validate this approach by applying it to a simple hybrid system, the well-known thermostat example

We advocate the need for automated support to System Requirement Analysis in the development of time- and safety-critical computer-based systems. To this end we pursue an approach based on deductive analysis: high-level, real-world entities and notions, such as events, states, finite variability, cause-effect relations, are modeled through the temporal logic TRIO, and the resulting deductive system is implemented by means of the theorem prover PVS. Throughout the paper, the constructs and features of the deductive system are illustrated and validated by applying them to the well-known example of the Generalized Railway Crossing.