Abstract In this work, we present an industrial case study of deadlock avoidance in the context of automated warehouse logistics. In particular, we consider systems of Automated Guided Vehicles (AGVs) in which semi-autonomous robots move inside a facility along a predefined set of paths. The paper introduces a novel formalization of AGV systems that models the physical setup of the AGV system more accurately compared to previous approaches. In particular, our modeling approach captures movement restrictions due to physical proximity of vehicles regardless of the logical connectivity of the guide path network. The paper provides and compares three different encodings of such models as transition systems, which enable symbolic analysis of the system via Binary Decision Diagrams (BDDs). Based on these encodings we perform deadlock avoidance for warehouse layouts of both synthetic and real-world origin.

Abstract Active automata learning enables model-based testing and verification of black-box systems by automatically constructing models from observations via interactions with the system. As interactions are usually expensive, active algorithms attempt to perform as few interactions as possible to learn a given system. However, many such algorithms struggle when confronted with noise, such as message loss, when learning otherwise deterministic systems. We investigate and adapt different algorithms to learn deterministic automata in a noisy setting. One of these is a novel active algorithm based on our previous passive Partial Max-SAT algorithm. In our analysis, we demonstrate techniques to lower the required number of interactions and order the evaluated algorithms accordingly. Finally, we show that the necessary interactions can be further reduced when leaving the classical active learning framework.

With the servitization of business, understanding how users experience services becomes a crucial success factor for companies. Therefore, there is a need to include feedback from user experiences in the software engineering process. Behavioral models of user journeys, describing how users experience their interaction with a service, can provide insights and potentially improve services. In this paper, we investigate techniques that allow the automatic generation of behavioral models from user interactions with a service, recorded in an event log. We first compare two established techniques that generate behavioral models from a given event log: automata learning and process mining. Afterward, we present a novel, hybrid method that combines both automata learning and process mining methods to overcome their limitations. For the existing techniques, we present methods to learn models of user journeys and evaluate the accuracy of the resulting models. We then compare these techniques with our novel method for the automatic extraction of user journey models from the event logs of digital services. We assess the practical applicability of all techniques by evaluating real-world applications. Our results show that process mining techniques rely on expert knowledge, while automata learning techniques depend on the distribution of events in the given event log. We further show that the proposed hybrid technique combines the strengths of both process mining and automata learning, automatically selecting the best method and parameter settings for a given event log to learn very accurate models.

Abstract AALpy is a well-established open-source automata learning library written in Python with a focus on active learning of systems with IO behavior. It provides a wide range of state-of-the-art algorithms for different automaton types ranging from fully deterministic to probabilistic automata. In this work, we present the recent addition of a generalized implementation of an important method from the domain of passive automata learning: state-merging in the red-blue framework. Using a common internal representation for different automaton types allows for a general and highly configurable implementation of the red-blue framework. We describe how to define and execute state-merging algorithms using AALpy, which reduces the implementation effort for state-merging algorithms mainly to the definition of compatibility criteria and scoring. This aids the implementation of both existing and novel algorithms. In particular, defining some existing state-merging algorithms from the literature with AALpy only takes a few lines of code.

Reinforcement learning from demonstrations (RLfD) is a promising approach to improve the exploration efficiency of reinforcement learning (RL) by learning from expert demonstrations in addition to interactions with the environment. In this paper, we propose a framework that combines techniques from search-based testing with RLfD with the goal to raise the level of dependability of RL policies and to reduce human engineering effort. Within our framework, we provide methods for efficiently training, evaluating, and repairing RL policies. Instead of relying on the costly collection of demonstrations from (human) experts, we automatically compute a diverse set of demonstrations via search-based fuzzing methods and use the fuzz demonstrations for RLfD. To evaluate the safety and robustness of the trained RL agent, we search for safety-critical scenarios in the black-box environment. Finally, when unsafe behavior is detected, we compute demonstrations through fuzz testing that represent safe behavior and use them to repair the policy. Our experiments show that our framework is able to efficiently learn high-performing and safe policies without requiring any expert knowledge.

The mining of models from data finds widespread use in industry. There exists a variety of model inference methods for perfectly deterministic behaviour, however, in practice, the provided data often contains noise due to faults such as message loss or environmental factors that many of the inference algorithms have problems dealing with. We present a novel model mining approach using Partial Max-SAT solving to infer the best possible automaton from a set of noisy execution traces. This approach enables us to ignore the minimal number of presumably faulty observations to allow the construction of a deterministic automaton. No pre-processing of the data is required. The method's performance as well as a number of considerations for practical use are evaluated, including three industrial use cases, for which we inferred the correct models.

Techniques like deep reinforcement learning (DRL) enable autonomous agents to solve tasks in complex environments automatically through learning. Despite their potential, neural-network-based decision-making policies are hard to understand and test. To ease the adoption of such techniques, we learn automata models of environmental behavior under the control of an agent. These models provide insights into the decisions faced by agents and a basis for testing. To scale automata learning to environments with complex and continuous dynamics, we compute an abstract state-space representation through dimensionality reduction and clustering of observed environmental states. The stochastic transitions are learned via passive automata learning from agent-environment interactions. Furthermore, we iteratively sample additional tra-jectories to enhance the learned model's accuracy. We demonstrate the potential of our automata learning frame-work by (1) solving popular RL benchmark problems and (2) applying it for differential testing of DRL agents. Our results show that the learned models are sufficiently precise to compute policies that solve the respective control tasks. Yet the models are sufficiently general for coverage-guided testing, where we reveal significant differences in the functional failure frequency of pairs of DRL agents.

Automata learning enables model-based analysis of black-box systems by automatically constructing models from system observations, which are often collected via testing. The required testing budget to learn adequate models heavily depends on the applied learning and testing techniques. Test cases executed for learning (1) collect behavioural information and (2) falsify learned hypothesis automata. Falsification test-cases are commonly selected through conformance testing. Active learning algorithms additionally implement test-case selection strategies to gain information, whereas passive algorithms derive models solely from given data. In an active setting, such algorithms require external test-case selection, like repeated conformance testing to extend the available data. There exist various approaches to learning and conformance testing, where interdependencies among them affect performance. We investigate the performance of combinations of six learning algorithms, including a passive algorithm, and seven testing algorithms by performing experiments using 153 benchmark models. We discuss insights regarding the performance of different configurations for various types of systems. Our findings may provide guidance for future users of automata learning. For example, counterexample processing during learning strongly impacts efficiency, which is further affected by testing approach and system type. Testing with the random Wp-method performs best overall, while mutation-based testing performs well on smaller models.

Abstract In this article, we present a novel approach to learning finite automata with the help of recurrent neural networks. Our goal is not only to train a neural network that predicts the observable behavior of an automaton but also to learn its structure, including the set of states and transitions. In contrast to previous work, we constrain the training with a specific regularization term. We iteratively adapt the architecture to learn the minimal automaton, in the case where the number of states is unknown. We evaluate our approach with standard examples from the automata learning literature, but also include a case study of learning the finite-state models of real Bluetooth Low Energy protocol implementations. The results show that we can find an appropriate architecture to learn the correct minimal automata in all considered cases.

Abstract Porting software to new target architectures is a common challenge, particularly when dealing with low-level functionality in drivers or OS kernels that interact directly with hardware. Traditionally, adapting code for different hardware platforms has been a manual and error-prone process. However, with the growing demand for dependability and the increasing hardware diversity in systems like the IoT, new software development approaches are essential. This includes rigorous methods for verifying and automatically porting Real-Time Operating Systems (RTOS) to various devices. Our framework addresses this challenge through formal methods and code generation for embedded RTOS. We demonstrate a hardware-specific part of a kernel model in Event-B, ensuring correctness according to the specification. Since hardware details are only added in late modeling stages, we can reuse most of the model and proofs for multiple targets. In a proof of concept, we refine the generic model for two different architectures, also ensuring safety and liveness properties. We then showcase automatic low-level code generation from the model. Finally, a hardware-independent factorial function model illustrates more potential of our approach.

Abstract Black-box systems are inherently hard to verify. Many verification techniques, like model checking, require formal models as a basis. However, such models often do not exist, or they might be outdated. Active automata learning helps to address this issue by offering to automatically infer formal models from system interactions. Hence, automata learning has been receiving much attention in the verification community in recent years. This led to various efficiency improvements, paving the way toward industrial applications. Most research, however, has been focusing on deterministic systems. In this article, we present an approach to efficiently learn models of stochastic reactive systems. Our approach adapts $$L^*$$ L ∗ -based learning for Markov decision processes, which we improve and extend to stochastic Mealy machines. When compared with previous work, our evaluation demonstrates that the proposed optimizations and adaptations to stochastic Mealy machines can reduce learning costs by an order of magnitude while improving the accuracy of learned models.

Evaluation of deep reinforcement learning (RL) is inherently challenging. Especially the opaqueness of learned policies and the stochastic nature of both agents and environments make testing the behavior of deep RL agents difficult. We present a search-based testing framework that enables a wide range of novel analysis capabilities for evaluating the safety and performance of deep RL agents. For safety testing, our framework utilizes a search algorithm that searches for a reference trace that solves the RL task. The backtracking states of the search, called boundary states, pose safety-critical situations. We create safety test-suites that evaluate how well the RL agent escapes safety-critical situations near these boundary states. For robust performance testing, we create a diverse set of traces via fuzz testing. These fuzz traces are used to bring the agent into a wide variety of potentially unknown states from which the average performance of the agent is compared to the average performance of the fuzz traces. We apply our search-based testing approach on RL for Nintendo's Super Mario Bros.

Abstract Automata learning is a technique to automatically infer behavioral models of black-box systems. Today’s learning algorithms enable the deduction of models that describe complex system properties, e.g., timed or stochastic behavior. Despite recent improvements in the scalability of learning algorithms, their practical applicability is still an open issue. Little work exists that actually learns models of physical black-box systems. To fill this gap in the literature, we present a case study on applying automata learning on the Bluetooth Low Energy (BLE) protocol. It shows that not only the size of the system limits the applicability of automata learning. Also, the interaction with the system under learning creates a major bottleneck that is rarely discussed. In this article, we propose a general automata learning architecture for learning a behavioral model of the BLE protocol implemented by a physical device. With this framework, we can successfully learn the behavior of six investigated BLE devices. Furthermore, we extended the learning technique to learn security critical behavior, e.g., key-exchange procedures for encrypted communication. The learned models depict several behavioral differences and inconsistencies to the BLE specification. This shows that automata learning can be used for fingerprinting black-box devices, i.e., characterizing systems via their specific learned models. Moreover, learning revealed a crashing scenario for one device.

The number of devices in the Internet of Things (IoT) immensely grew in recent years. A frequent challenge in the assurance of the dependability of IoT systems is that components of the system appear as a black box. This paper presents a semi-automatic testing methodology for black-box systems that combines automata learning and fuzz testing. Our testing technique uses stateful fuzzing based on a model that is automatically inferred by automata learning. Applying this technique, we can simultaneously test multiple implementations for unexpected behavior and possible security vulnerabilities.We show the effectiveness of our learning-based fuzzing technique in a case study on the MQTT protocol. MQTT is a widely used publish/subscribe protocol in the IoT. Our case study reveals several inconsistencies between five different MQTT brokers. The found inconsistencies expose possible security vulnerabilities and violations of the MQTT specification.

Abstract Automata learning techniques automatically generate systemmodels fromtest observations. Typically, these techniques fall into two categories: passive and active. On the one hand, passive learning assumes no interaction with the system under learning and uses a predetermined training set, e.g., system logs. On the other hand, active learning techniques collect training data by actively querying the system under learning, allowing one to steer the discovery ofmeaningful information about the systemunder learning leading to effective learning strategies. A notable example of active learning technique for regular languages is Angluin’s L ∗ -algorithm. The L ∗ -algorithm describes the strategy of a student who learns the minimal deterministic finite automaton of an unknown regular language L by asking a succinct number of queries to a teacher who knows L . In this work, we study L ∗ -based learning of deterministic Markov decision processes, a class of Markov decision processes where an observation following an action uniquely determines a successor state. For this purpose, we first assume an ideal setting with a teacher who provides perfect information to the student. Then, we relax this assumption and present a novel learning algorithm that collects information by sampling execution traces of the system via testing. Experiments performed on an implementation of our sampling-based algorithm suggest that our method achieves better accuracy than state-of-the-art passive learning techniques using the same amount of test obser vations. In contrast to existing learning algorithms which assume a predefined number of states, our algorithm learns the complete model structure including the state space.

Special issue on testing extra-functional propertiesCo-located with the 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017) in Tokyo, we started with and organized the first International Workshop on Testing Extra-Functional Properties and Quality Characteristics of Software Systems (ITEQS) †.The importance of having a dedicated forum discussing various aspects of testing EFPs becomes more apparent considering the following points.With the ever-increasing role of computer systems in our daily life, we rely more and more on the services that are provided by a software.As a consequence, the expectations and demands regarding the quality of these services are also dramatically growing.In this context, the success and correctness of a software product may not only be dependent on the logical correctness of its functions but also on their other quality attributes such as performance, security, safety, availability and robustness.Such system characteristics, which are referred to and captured as extra-functional properties (EFPs), or non-functional properties, have determinant importance particularly in resource constrained systems.For instance, in the real-time embedded domain, there can be limitations on available memory, CPU and processing capacity, power consumption and so on, that need to be considered along with timing and security requirements of an application.These systems, therefore, need to be tested with a special attention to EFPs.Testing a system with respect to its EFPs, however, poses specific challenges, and traditional functional testing methods and approaches may not simply be applicable.Examples of such challenges are fault localization, the need to have appropriate techniques for different types of EFPs, the role and impact of the environment in testing EFPs, observability and testability issues, coverage and test-stop criteria, modelling EFPs and generating meaningful test cases, test oracles for security and privacy that involve hyperproperties, etc.Considering the peculiarities and challenges of testing EFPs, the main purpose of ITEQS has been to provide a well-focused forum with the goal of bringing together researchers and practitioners to share ideas, identify challenges, propose solutions and techniques, and in general, expand the state-of-the-art and practice in testing EFPs and quality characteristics of software systems.Since 2017 and until today, ITEQS has been held each year co-located with the ICST conference, attracting different articles and audience discussions, having keynote speeches from well-known researchers in the field, and also panel discussions on specific themes related to the overall topic of the workshop.This special issue on testing EFPs in the Software Testing, Verification and Reliability Journal was established with the ITEQS 2018 workshop, inviting selected best papers from both ITEQS 2017 and 2018 to submit extensions of their work and also being open to any other external high-quality research articles on the topic.The first paper, "An Exploration of Effective Fuzzing for Side-channel Cache Leakage" by Tiyash Basu, Chundong Wang and Sudipta Chattopadhyay focuses on the problem of validating software systems against both cache timing-based and access-based attacks.They present a coverage metric and a simulated annealing-based test generation approach that explores the cache behaviour.The approach has been evaluated against two state-of-the-art fuzz testing tools in both a †

Model checking has a long-standing tradition in software verification. Given a system design it checks whether desired properties are satisfied. Unlike testing, it cannot be applied in a black-box setting. To overcome this limitation Peled et al. introduced black-box checking, a combination of testing, model inference and model checking. The technique requires systems to be fully deterministic. For stochastic systems, statistical techniques are available. However, they cannot be applied to systems with non-deterministic choices. We present a black-box checking technique for stochastic systems that allows both, non-deterministic and probabilistic behaviour. It involves model inference, testing and probabilistic model-checking. Here, we consider reachability checking, i.e., we infer near-optimal input-selection strategies for bounded reachability.

System verification is often hindered by the absence of formal models. Peled et al. proposed black-box checking as a solution to this problem. This technique applies active automata learning to infer models of systems with unknown internal structure. This kind of learning relies on conformance testing to determine whether a learned model actually represents the considered system. Since conformance testing may require the execution of a large number of tests, it is considered the main bottleneck in automata learning. In this paper, we describe a randomised conformance testing approach which we extend with fault-based test selection. To show its effectiveness we apply the approach in learning experiments and compare its performance to a well-established testing technique, the partial W-method. This evaluation demonstrates that our approach significantly reduces the cost of learning. In multiple experiments, we reduce the cost by at least one order of magnitude.

Property-based testing is well suited for web-service applications, which was already shown in various case studies. For example, it has been demonstrated that JSON schemas can be used to automatically derive test case generators for web forms. In this work, we present a test case generation approach for a rule engine-driven web-service application. Business-rule models serve us as input for property-based testing. We parse these models to automatically derive generators for sequences of web-service requests together with their required form data. Property-based testing is mostly applied in the context of functional programming. Here, we define our properties in an object-oriented style in C# and its tool FsCheck. We apply our method to the business-rule models of an industrial web-service application in the automotive domain.

Since computers have become increasingly more powerful, users are less willing to accept slow responses of systems. Hence, performance testing is important for interactive systems. However, it is still challenging to test if a system provides acceptable performance or can satisfy certain response-time limits, especially for different usage scenarios. On the one hand, there are performance-testing techniques that require numerous costly tests of the system. On the other hand, model-based performance analysis methods have a doubtful model quality. Hence, we propose a combined method to mitigate these issues. We learn response-time distributions from test data in order to augment existing behavioral models with timing aspects. Then, we perform statistical model checking with the resulting model for a performance prediction. Finally, we test the accuracy of our prediction with hypotheses testing of the real system. Our method is implemented with a property-based testing tool with integrated statistical model checking algorithms. We demonstrate the feasibility of our techniques in an industrial case study with a web-service application.

Black-box components conceal parts of software execution paths, which makes systematic testing, e. g., via symbolic execution, difficult. In this paper, we use automata learning to facilitate symbolic execution in the presence of black-box components. We substitute black-boxes in a software system with learned automata that model them, enabling us to symbolically execute program paths that run through black-boxes. We show that applying the approach on real-world software systems incorporating black-boxes increases code coverage when compared to standard techniques.

No abstract available.

In recent years, statistical model checking (SMC) has become increasingly popular, because it scales well to larger stochastic models and is relatively simple to implement. SMC solves the model checking problem by simulating the model for finitely many executions and uses hypothesis testing to infer if the samples provide statistical evidence for or against a property. Being based on simulation and statistics, SMC avoids the state-space explosion problem well-known from other model checking algorithms. In this paper we show how SMC can be easily integrated into a property-based testing framework, like FsCheck for C#. As a result we obtain a very flexible testing and simulation environment, where a programmer can define models and properties in a familiar programming language. The advantages: no external modelling language is needed and both stochastic models and implementations can be checked. In addition, we have access to the powerful test-data generators of a property-based testing tool. We demonstrate the feasibility of our approach by repeating three experiments from the SMC literature.

This paper presents a learning-based approach to detecting failures in reactive systems. The technique is based on inferring models of multiple implementations of a common specification which are pair-wise cross-checked for equivalence. Any counterexample to equivalence is flagged as suspicious and has to be analysed manually. Hence, it is possible to find possible failures in a semi-automatic way without prior modelling. We show that the approach is effective by means of a case study. For this case study, we carried out experiments in which we learned models of five implementations of MQTT brokers/servers, a protocol used in the Internet of Things. Examining these models, we found several violations of the MQTT specification. All but one of the considered implementations showed faulty behaviour. In the analysis, we discuss effectiveness and also issues we faced.

Deterministic timed automata are strictly less expressive than their non-deterministic counterparts, which are again less expressive than those with silent transitions. As a consequence, timed automata are in general non-determinizable. This is unfortunate since deterministic automata play a major role in model-based testing, observability and implementability. However, by bounding the length of the traces in the automaton, effective determinization becomes possible. We propose a novel procedure for bounded determinization of timed automata. The procedure unfolds the automata to bounded trees, removes all silent transitions and determinizes via disjunction of guards. The proposed algorithms are optimized to the bounded setting and thus are more efficient and can handle a larger class of timed automata than the general algorithms. We show how to apply the approach in a fault-based test-case generation method, called model-based mutation testing, that was previously restricted to deterministic timed automata. The approach is implemented in a prototype tool and evaluated on several scientific examples and one industrial case study. To our best knowledge, this is the first implementation of this type of procedure for timed automata.

We propose a framework for requirement-driven test generation that combines contract-based interface theories with model-based testing. We design a specification language, requirement interfaces, for formalizing different views (aspects) of synchronous data-flow systems from informal requirements. Various views of a system, modeled as requirement interfaces, are naturally combined by conjunction. We develop an incremental test generation procedure with several advantages. The test generation is driven by a single requirement interface at a time. It follows that each test assesses a specific aspect or feature of the system, specified by its associated requirement interface. Since we do not explicitly compute the conjunction of all requirement interfaces of the system, we avoid state space explosion while generating tests. However, we incrementally complete a test for a specific feature with the constraints defined by other requirement interfaces. This allows catching violations of any other requirement during test execution, and not only of the one used to generate the test. This framework defines a natural association between informal requirements, their formal specifications, and the generated tests, thus facilitating traceability. Finally, we introduce a fault-based test-case generation technique, called model-based mutation testing, to requirement interfaces. It generates a test suite that covers a set of fault models, guaranteeing the detection of any corresponding faults in deterministic systems under test. We implemented a prototype test generation tool and demonstrate its applicability in two industrial use cases.

In recent years statistical model checking (SMC) became increasingly popular, mainly because it does not suffer from one of the major problems that limits traditional model checking, the so called state-space-explosion problem. SMC solves this problem by simulating a stochastic model for finitely many executions. There exist a number of SMC tools, but they require the user to learn a specific modelling language and a particular (temporal) logic to express properties. In this paper we propose a more flexible application of SMC, where both the model and the properties can be defined in a programming language. The technique builds upon the well-known property-based testing approach. We use the programming language C# and its associated tool FsCheck to demonstrate our approach. A stochastic counter serves as illustrating example.

Timed Automata are established specification models for real-time systems. One of their main advantages is composability, allowing the modular specification of different aspects of a system via communicating timed automata. Composed together, these automata specify the behavior of a whole component or system. In previous work, we developed a technique to determinize a single timed automaton, by unfolding it and bounding ourselves to an observable depth k. Within this paper we expand our approach, enabling the efficient bounded determinization of networks of timed automata. We realize an on-the-fly algorithm that performs at each level of unfolding the following tasks: building the product, hiding the communication, removing silent transitions, and determinizing. In contrast to the previous work, this on-the-fly algorithm only needs to traverse the state-space exactly once. We implemented the algorithm in the model-based testing tool MoMuT::TA and demonstrate and evaluate our implementation on a case study.

Model-based mutation testing (MBMT) is a promising testing methodology that relies on a model of the system under test (SUT) to create test cases. Hence, MBMT is a so-called black-box testing approach. It also is fault based, as it creates test cases that are guaranteed to reveal certain faults: after inserting a fault into the model of the SUT, it looks for a test case revealing this fault. This turns MBMT into one of the most powerful and versatile test case generation approaches available as its tests are able to demonstrate the absence of certain faults, can achieve both, control-flow and data-flow coverage of model elements, and also may include information about the behaviour in the failure case. The latter becomes handy whenever the test execution framework is bound in the number of observations it can make and - as a consequence - has to restrict them. However, this versatility comes at a price: MBMT is computationally expensive. The tool MoMuT::UML (https://www.momut.org) is the result of a multi-year research effort to bring MBMT from the academic drawing board to industrial use. In this paper we present the current stable version, share the lessons learnt when applying two generations of MoMuT::UML in an industrial setting, and give an outlook on the upcoming, third,generation.

Summary This article presents the techniques and results of a novel model‐based test case generation approach that automatically derives test cases from UML state machines. The main contribution of this article is the fully automated fault‐based test case generation technique together with two empirical case studies derived from industrial use cases. Also, an in‐depth evaluation of different fault‐based test case generation strategies on each of the case studies is given and a comparison with plain random testing is conducted. The test case generation methodology supports a wide range of UML constructs and is grounded on the formal semantics of Back's action systems and the well‐known input–output conformance relation. Mutation operators are employed on the level of the specification to insert faults and generate test cases that will reveal the faults inserted. The effectiveness of this approach is shown and it is discussed how to gain a more expressive test suite by combining cheap but undirected random test case generation with the more expensive but directed mutation‐based technique. Finally, an extensive and critical discussion of the lessons learnt is given as well as a future outlook on the general usefulness and practicability of mutation‐based test case generation. Copyright © 2014 John Wiley & Sons, Ltd.

In this paper we propose the combination of several techniques into an agile formal development process: model-based testing, formal models, refinement of models, model checking, and test-driven development. The motivation is a smooth integration of formal techniques into an existing development cycle. Formal models are used to generate abstract test cases. These abstract tests are verified against requirement properties by means of model checking. The motivation for verifying the tests and not the model is two-fold: (1) in a typical safety-certification process the test cases are essential, not the models, (2) many common modelling tools do not provide a model checker. We refine the models, check refinement, and generate additional test cases capturing the newly added details. The final refinement step from a model to code is done with classical test-driven development. Hence, a developer implements one generated and formally verified test case after another, until all tests pass. The process is scalable to actual needs. Emphasis can be shifted between formal refinement of models and test-driven development. A car alarm system serves as a demonstrating case-study. We use Back's Action Systems as modelling language and mutation analysis for test case generation. We define refinement as input-output conformance (ioco). Model checking is done with the CADP toolbox.

Model-based mutation testing uses altered models to generate test cases that are able to detect whether a certain fault has been implemented in the system under test. For this purpose, we need to check for conformance between the original and the mutated model. We have developed an approach for conformance checking of action systems using constraints. Action systems are well-suited to specify reactive systems and may involve non-determinism. Expressing their semantics as constraints for the purpose of conformance checking is not totally straight forward. This paper presents some pitfalls that hinder the way to a sound encoding of semantics into constraint satisfaction problems and gives solutions for each problem.

Europe's industry in embedded system design is currently aiming for a better integration of tools that support their development, validation and verification processes. The idea is to combine model-driven development with model-based testing and model-based analysis. The interoperability of tools shall be achieved with the help of meta-models that facilitate the mapping between different modelling notations. However, the syntactic and semantic integration of tools is a complex and costly task. A common problem is that different tools support different subsets of a language. Furthermore, semantic differences are a major obstacle to sound integration efforts. In this paper we advocate an alternative, more pragmatic approach. We propose the exchange of test cases generated from the models instead of exchanging the models themselves. The advantage is that test cases have a much simpler syntax and semantics, and hence, the mapping between different tools is easier to implement and to maintain. With a formal testing approach with adequate testing criteria a set of test cases can be viewed as partial models that can be formally analysed. We demonstrate an integration of our test case generator Ulysses with the CADP toolbox by means of test case exchange. We generate test cases in Ulysses and verify properties in CADP. We also generate test cases in CADP and perform a mutation analysis in Ulysses.

This paper presents the techniques and results of a novel model-based test case generation approach that automatically derives test cases from UML state machines. Mutation testing is applied on the modeling level to generate test cases. We present the test case generation approach, discuss the tool chain, and present the properties of the generated test cases. The main contribution of this paper is an empirical study of a car alarm system where different strategies for killing mutants are compared. We present detailed figures on the effectiveness of the test case generation technique. Although UML serves as an input language, all techniques are grounded on solid foundations: we give UML state transition diagrams a formal semantics by mapping them to Back's action systems.

Model-based testing is a well known technique that allows one to validate the correctness of software with respect to its model. If a lot of data is involved, symbolic techniques usually outperform explicit data enumeration. In this paper, we focus on a new symbolic test case generation technique. Our approach is based on symbolic execution and on satisfiability (modulo theory; SMT) solving. Our work was motivated by the complete failure of a well-known existing symbolic test case generator to produce any test cases for an industrial Session Initiation Protocol (SIP) implementation. Hence, we have replaced the BDD-based analysis of the existing tool with a combination of symbolic execution and SMT solving. Our new tool generates the test cases for SIP in seconds. However, further experiments showed that our approach is not a substitutive but a complementary approach: we present the technique and the results obtained for two protocol specifications, the first supporting our new technique, the second being witness for the classic BDD-technique.

The complex interactions appearing in service-oriented computing make coordination a key concern in service-oriented systems. In this paper, we present a fault-based method to generate test cases for component connectors from specifications. For connectors, faults are caused by possible errors during the development process, such as wrongly used channels, missing or redundant subcircuits, or circuits with wrongly constructed topology. We give test cases and connectors a unifying formal semantics by using the notion of design, and generate test cases by solving constraints obtained from the specification and faulty connectors. A prototype symbolic test case generator serves to demonstrate the automatizing of the approach.

Abstract This paper presents a theory of testing that integrates into Hoare and He’s Unifying Theory of Programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. Having such a refinement order that integrates test cases, we develop a testing theory for fault-based testing. Fault-based testing uses test data designed to demonstrate the absence of a set of pre-specified faults. A well-known fault-based technique is mutation testing. In mutation testing, first, faults are injected into a program by altering (mutating) its source code. Then, test cases that can detect these errors are designed. The assumption is that other faults will be caught, too. In this paper, we apply the mutation technique to both, specifications and programs. Using our theory of testing, two new test case generation laws for detecting injected (anticipated) faults are presented: one is based on the semantic level of UTP design predicates, the other on the algebraic properties of a small programming language.

Various research prototypes and a well-founded theory of model based testing (MBT) suggests the application of MBT to real-world problems. In this article we report on applying the well-known TGV tool for protocol conformance testing of a Session Initiation Protocol (SIP) server. Particularly, we discuss the performed abstractions along with corresponding rationales. Furthermore, we show how to use structural and fault-based techniques for test purpose design. We present first empirical results obtained from applying our test cases to a commercial implementation and to a popular open source implementation of a SIP Registrar. Notably, in both implementations our input output labeled transition system model proved successful in revealing severe violations of the protocol.

Research on non-structural system group decision-making problems largely depends on the knowledge and experience of the experts for tactical analysis. The usual method of voting may result in a great loss of information in case of much renunciation, and the accuracy of voting can therefore be directly influenced.This paper proposes a new solution to non-structural system group decision-making problems by taking advantage of the characteristics of correlate and the information easy to lose to make an overall analysis of the ayes, blackballs and renunciation polls for an accurate result.

Abstract This article discusses mutation testing strategies in the context of refinement. Here, a novel generalisation of mutation testing techniques is presented to be applied to contracts ranging from formal specifications to programs. It is demonstrated that refinement and its dual abstraction are the key notions leading to a precise and yet simple theory of mutation testing. The refinement calculus of Back and von Wright is used to express concepts like contracts, useful mutations, test cases and test coverage.