Abstract This is the second issue in the new “Competitions and Challenges” (CoCha) theme of the International Journal on Software Tools for Technology Transfer. The new theme was established to support competitions and challenges with an appropriate publication venue. The first issue presented the competition on software testing Test-Comp 2019, which was part of the TOOLympics 2019 event. In this second issue for TOOLympics, we present selected competition reports. The TOOLympics event took place as part of the 25-years celebration of the conference TACAS. The goal of the event was to provide an overview of competitions and challenges in the area of formal methods.

The Model Checking Contest (MCC) is an annual competition of software tools for model checking. Tools must process an increasing benchmark gathered from the whole community and may participate in various examinations: state space generation, computation of global properties, computation of some upper bounds in the model, evaluation of reachability formulas, evaluation of CTL formulas, and evaluation of LTL formulas. For each examination and each model instance, participating tools are provided with up to 3600 s and 16 gigabyte of memory. Then, tool answers are analyzed and confronted to the results produced by other competing tools to detect diverging answers (which are quite rare at this stage of the competition, and lead to penalties). For each examination, golden, silver, and bronze medals are attributed to the three best tools. CPU usage and memory consumption are reported, which is also valuable information for tool developers.

Evaluation of scientific contributions can be done in many different ways. For the various research communities working on the verification of systems (software, hardware, or the underlying involved mechanisms), it is important to bring together the community and to compare the state of the art, in order to identify progress of and new challenges in the research area. Competitions are a suitable way to do that. The first verification competition was created in 1992 (SAT competition), shortly followed by the CASC competition in 1996. Since the year 2000, the number of dedicated verification competitions is steadily increasing. Many of these events now happen regularly, gathering researchers that would like to understand how well their research prototypes work in practice. Scientific results have to be reproducible, and powerful computers are becoming cheaper and cheaper, thus, these competitions are becoming an important means for advancing research in verification technology. TOOLympics 2019 is an event to celebrate the achievements of the various competitions, and to understand their commonalities and differences. This volume is dedicated to the presentation of the 16 competitions that joined TOOLympics as part of the celebration of the $$25^{ th }$$ anniversary of the TACAS conference.

Over the last decade, parallel SATisfiability solving has been widely studied from both theoretical and practical aspects. There are two main approaches. First, divide-and-conquer ( D&C ) splits the search space, each solver being in charge of a particular subspace. The second one, portfolio launches multiple solvers in parallel, and the first to find a solution ends the computation. However although D&C based approaches seem to be the natural way to work in parallel, portfolio ones experimentally provide better performances. An explanation resides on the difficulties to use the native formulation of the SAT problem ( i.e., the CNF form) to compute an a priori good search space partitioning ( i.e., all parallel solvers process their subspaces in comparable computational time). To avoid this, dynamic load balancing of the search subspaces is implemented. Unfortunately, this is difficult to compare load balancing strategies since state-of-the-art SAT solvers appropriately dealing with these aspects are hardly adaptable to various strategies than the ones they have been designed for. This paper aims at providing a way to overcome this problem by proposing an implementation and evaluation of different types of divide-and-conquer inspired from the literature. These are relying on the Painless framework, which provides concurrent facilities to elaborate such parallel SAT solvers. Comparison of the various strategies are then discussed.

Building a certification authority that is both decentralized and fully reliable is impossible. However, the limitation thus imposed on scalability is unacceptable for many types of information systems, such as e-government services, which require an infrastructure able to support heavy computation loads while remaining highly reliable. Our scalable approach opts for the next best thing to full reliability: a certification authority with a probability of arbitrary failure so low that, in practice, false positives should never occur.

While Service Oriented Architectures (SOAs) are for many parts deployed online, and today often in a cloud, the testing of the systems still happens mostly locally. In this paper, we want to present the MIDAS Testing as a Service (TaaS), a cloud platform for the testing of SOAs. We focus on the testing of whole SOA orchestrations, a complex task due to the number of potential service interactions and the increasing complexity with each service that joins an orchestration. Since traditional testing does not scale well with such a complex setup, we employ a Model-based Testing (MBT) approach based on the Unified Modeling Language (UML) and the UML Testing Profile (UTP) within MIDAS. Through this, we provide methods for functional testing, security testing, and usage-based testing of service orchestrations. Through harnessing the computational power of the cloud, MIDAS is able to generate and execute complex test scenarios which would be infeasible to run in a local environment.

CosyVerif aims at gathering within a common framework various existing tools for specification and verification. It has been designed in order to 1) support different formalisms with the ability to easily create new ones, 2) provide a graphical user interface for every formalism, 3) include verification tools called via the graphical interface or via an API as a Web service, and 4) offer the possibility for a developer to integrate his/her own tool without much effort, also allowing it to interact with the other tools. Several tools have already been integrated for the formal verification of (extensions of) Petri nets and timed automata.

SUMMARY Safety‐critical systems are used in many domains (military, avionics, aerospace, etc.) and handle critical data in hostile environments. To prevent data access by unauthorized subjects, they must protect and isolate information so that only allowed entities can read or write information. However, because of their increased number of functionalities, safety‐critical systems design becomes more complex; this increases difficulties in the design and the verification of security functions and potential error in their implementation. The multiple independent levels of security (MILS) approach introduces rules and guidelines for the design of secure systems. It isolates data according to their security levels, reducing system complexity to ease development. However, there is no approach addressing the whole development of MILS systems from high‐level specification (application components with their security levels) to the final implementation (code that executes application functions and provide security mechanisms). This paper presents a complete development approach for the design, verification and implementation of MILS architectures. It aims at providing a complete framework to build secure applications based on MILS guidelines. We describe security concerns using a modeling language, verify security requirements and automatically implement the system code generation techniques and a MILS‐compliant operating system that provides security functions. Copyright © 2012 John Wiley & Sons, Ltd.

SUMMARY The complexity of modern embedded systems increases as they incorporate new concerns such as distribution and mobility. These new features need to be considered as early as possible in the software development life cycle. Model driven engineering promotes an intensive use of models and is now widely seen as a solution to master the development of complex systems such as embedded ones. Component‐based software engineering is another major trend that gains acceptance in the embedded world because of its properties such as reuse, modularity, and flexibility. This article proposes the Flex‐eWare component model (FCM) for designing and implementing modern embedded systems. The FCM unifies model driven engineering and component‐based software engineering and has been evaluated in several application domains with different requirements: wireless sensor networks, distributed client/server applications, and control systems for electrical devices. This approach highlights a new concept: flexibility points that arise at several stages of the development process, that is, in the model (design phase), in the execution platform, and during the execution itself. This flexibility points are captured with model libraries that can extend the FCM. Copyright © 2011 John Wiley & Sons, Ltd.

AADL is an architecture description language intended for model-based engineering of high-integrity systems. The AADL Behavior Annex is an extension allowing the refinement of behavioral aspects described through AADL. When implementing Distributed Real-time Embedded system, fault tolerance concerns are integrated by applying replication patterns. We considered a simplified design of the primary backup replication pattern to express the modeling capabilities of AADL and its annex. Our contribution intends to give accurate description of the synchronization mechanisms integrated in this example.

Model driven engineering (MDE) and organic computing (OC) are fashion buzzwords these years. However, are the associated techniques in competition or complementary? We first provide some definitions about these terms and then present some elements suitable for discussion during the panel.

Modeling of distributed real-time embedded (DRE) systems allows one to evaluate models behavior or schedulability. However, assessing that a DRE system's behavior is correct in the causal domain is a challenge: one need to elaborate a mathematical abstraction suitable for checking properties like absence of deadlock or safety conditions (i.e. an invariant remains all over the execution). In this paper, we propose a global approach to building Petri Nets models from an architecture described using AADL. We consider the semantics of interacting entities defined by AADL, and show how to build corresponding Petri Nets models. Based on a case study, we show how the verification process could be automated and parameterized.

Shared decision diagram representations of a state-space provide efficient solutions for model-checking of large systems. However, decision diagram manipulation is tricky, as the construction procedure is liable to produce intractable intermediate structures (a.k.a peak effect). The definition of the so-called saturation method has empirically been shown to mostly avoid this peak effect, and allows verification of much larger systems. However, applying this algorithm currently requires deep knowledge of the decision diagram data structures. Hierarchical Set Decision Diagrams (SDD) are decision diagrams in which arcs of the structure are labeled with sets, themselves stored as SDD. This data structure offers an elegant and very efficient way of encoding structured specifications using decision diagram technology. It also offers, through the concept of inductive homomorphisms, flexibility to a user defining a symbolic transition relation. We show in this paper how, with very limited user input, the SDD library is able to optimize evaluation of a transition relation to produce a saturation effect at runtime. We build as an example an SDD model-checker for a compositional formalism: Instantiable Petri Nets (IPN). IPN define a type as an abstract contract. Labeled P/T nets are used as an elementary type. A composite type is defined to hierarchically contain instances (of elementary or composite type). To compose behaviors, IPN use classic label synchronization semantics from process calculi. With a particular recursive folding SDD are able to offer solutions for symmetric systems in logarithmic complexity with respect to other DD. Even in less regular cases, the use of hierarchy in the specification is shown to be well supported by SDD. Experimentations and performances are reported on some well known examples.

Embedded systems is an area that grows rapidly with new communication media such as smart-phones, house automation applications (that might finally come) and all other hidden systems we use everyday in cars, airplanes, etc. Moreover, in these last domains, there is a need for very safe development because such systems are often life-critical.

Building distributed deal-time embedded systems requires a stringent methodology, from early requirement capture to full implementation. However, there is a strong link between the requirements and the final implementation (e.g., scheduling and resource dimensioning). Therefore, a rapid prototyping process based on automation of tedious and error-prone tasks (analysis and code generation) is required to speed up the development cycle. In this article, we show how the AADL ( Architecture Analysis and Design Language ), which appeared in late 2004, helps solve these issues thanks to a dedicated tool suite. We then detail the prototyping process and its current implementation: Ocarina.

Model checking is a formal verification technique that allows to automatically prove that a system's behavior is correct. However it is often prohibitively expensive in time and memory complexity, due to the so-called state space explosion problem. We present a generic multithreaded and distributed infrastructure library designed to allow distribution of the model checking procedure over a cluster of machines. This library is generic, and is designed to allow encapsulation of any model checker in order to make it distributed. Performance evaluations are reported and clearly show the advantages of multi-threading to occupy processors while waiting for the network, with linear speedup over the number of processors.

Modern intelligent transport systems are large, distributed, and at least partially embedded systems. They raise new challenges through safe design because of their characteristics that are not easily managed informal methods. The purpose of this paper is to set up a methodology that selects appropriate techniques for the modeling and analysis of such systems. Our methodology relies on symmetric nets (formerly known as well formed Petri nets). We make intensive use of this formalism's capabilities to scale up analysis and set up a roadmap for the design of dedicated model checkers

Heterogeneous non-functional requirements of DRE system put a limit on middleware engineering; building an application-tailored middleware becomes a challenge. In this paper, we show how we use the PolyORB middleware and its architecture as a framework to implement DDS, the data distribution services (DDS) recently published by the OMG. We demonstrate how the architecture proposed by PolyORB enables a rapid implementation of this specification, and allows for extreme tailorability to support application requirements

Distributed real-time embedded systems (DRE) increasingly rely on COTS middleware to meet their distribution needs. Yet, there is a technology gap between the design of COTS middleware and the high-integrity constraints of real-time engineering. This puts a limit on the adoption of middleware by system families such as space or avionics. In this paper, we present our current work on the "schizophrenic middleware architecture", a highly tailorable middleware architecture, and its implementation PolyORB. We illustrate how it allows for support of real-time engineering guidelines, enforces determinism, allows for modeling and verification.

The implementation and maintenance of industrial applications have continuously become more and more difficult. In this context, one problem is the evaluation of complex systems. The IEEE defines prototyping as a development approach promoting the implementation of a pilot version of the intended product. This approach is a potential solution to the early evaluation of a system. It can also be used to avoid the shift between the description/specification of a system and its implementation. This brief introduction to the special section on rapid system prototyping illustrates a current picture of prototyping.

This paper proposes a methodology to build safe distributed systems that considers both conceptual and operational description aspects. At the conceptual level, we focus on the safety properties expected from the system. Such properties are stated and then verified. At the operational level, we focus on properties addressing the optimization of the generated code. Traceability between the two levels is managed in a satisfactory semi-automatic way. It preserves the properties proved at the first level and discards informations that are not relevant for code generation.

This paper presents a methodology that aims at the specification, verification and prototyping of large distributed systems. This methodology relies on H-COSTAM: a high level representation that supports hierarchy and focuses on message passing communication mechanisms. In order to enable validation based on a formal representation, a translation procedure to Petri net is proposed. We also show this can fit discrete application domains. Translation from discrete high level formalism into H-COSTAM is possible. We present an example with Estelle.

Rapid prototyping of parallel systems is of interest to quickly produce a parallel prototype. The emergence of distributed systems technology has enabled one to develop software systems distributed over large networks. Rapid prototyping must deal with real parallelism over a set of processors, either closely or loosely coupled. We describe an extension of the CPN/TAGADA project to manage distributed code generation over a set of CPU. To achieve a mapping of components over the target architecture, both hardware and software have to be described. We expose our technique and apply it to a multi producer and consumer example that is studied for several communication strategies.>

This paper presents a multi-formalism method for design and rapid prototyping of parallel systems. This approach mixes object paradigm and formal verification techniques. The method is based on enrichment and refinements, each one involving several intermediate representations bringing additional information. On this basis, a prototype is generated that may be either a prototype or a first operational version of the system or a model outlining design aspects. The prototype is defined using a generic architecture which makes it possible to implement the prototyping process for several languages without having to change the design approach.>

A rapid prototyping method for parallel systems is presented. The aim of the approach is to provide a rapid prototyping tool. Source formalism consists of coloured Petri nets. These allow powerful modelization and rely on a strong theoretical basis from which behavioural validation can be inferred. One major problem of rapid prototyping is environment integration. The authors propose a method which allows such integration. They present the methodology and illustrate it on a toy example.>