Search

Formal methods are promising for modeling and analyzing system requirements. However, applying formal methods to large-scale industrial projects is a remaining challenge. The industrial engineers are suffering from the lack of automated engineering methodologies to effectively conduct precise requirement models, and rigorously validate and verify (V&V) the generated models. To tackle this challenge, in this paper, we present a systematic engineering approach, named Formal Requirement Engineering Platform in Aircraft (FREPA), for formal requirement modeling and V\&V in the aerospace and aviation control domains. FREPA is an outcome of the seamless collaboration between the academy and industry over the last eight years. The main contributions of this paper include 1) an automated and systematic engineering approach FREPA to construct requirement models, validate and verify systems in the aerospace and aviation control domain, 2) a domain-specific modeling language AASRDL to describe the formal specification, and 3) a practical FREPA-based tool AeroReq which has been used by our industry partners. We have successfully adopted FREPA to seven real aerospace gesture control and two aviation engine control systems. The experimental results show that FREPA and the corresponding tool AeroReq significantly facilitate formal modeling and V&V in the industry. Moreover, we also discuss the experiences and lessons gained from using FREPA in aerospace and aviation projects., 12 pages, Published by FSE 2020

Testing a program to confirm whether it consistently implements its requirements specification is a necessary but time-consuming activity in software development. Automatic testing based on specifications can significantly alleviate the workload and cost, but faces a challenge of how to ensure that both the user's concerns in the specification and possible execution paths in the program are all covered. In this paper, we describe a new method, called "Vibration-Method" or simply "V-Method", for automatic generation of test cases and test oracle from model-based formal specifications, aiming to address this challenge. The proposed method is suitable for testing information systems in which rich data types are used. Supporting the principle of "divide and conquer", the method provides a specific technique for generating test cases based on functional scenarios defined in the specification, test case generation criteria, automatic test case generation algorithms, and a well-defined mechanism for deriving test oracle. We elaborate on the method by discussing how initial test cases can be automatically generated, how additional necessary test cases are produced using the "vibration" technique, and how a test oracle can be automatically derived for a group of test cases. We also describe a controlled experiment to evaluate the effectiveness of the method and discuss the important issues in relation to the performance and applicability of the method.

IoT devices are increasingly being implicated in cyber-attacks, raising community concern about the risks they pose to critical infrastructure, corporations, and citizens. In order to reduce this risk, the IETF is pushing IoT vendors to develop formal specifications of the intended purpose of their IoT devices, in the form of a Manufacturer Usage Description (MUD), so that their network behavior in any operating environment can be locked down and verified rigorously. This paper aims to assist IoT manufacturers in developing and verifying MUD profiles, while also helping adopters of these devices to ensure they are compatible with their organizational policies and track devices network behavior based on their MUD profile. Our first contribution is to develop a tool that takes the traffic trace of an arbitrary IoT device as input and automatically generates the MUD profile for it. We contribute our tool as open source, apply it to 28 consumer IoT devices, and highlight insights and challenges encountered in the process. Our second contribution is to apply a formal semantic framework that not only validates a given MUD profile for consistency, but also checks its compatibility with a given organizational policy. We apply our framework to representative organizations and selected devices, to demonstrate how MUD can reduce the effort needed for IoT acceptance testing. Finally, we show how operators can dynamically identify IoT devices using known MUD profiles and monitor their behavioral changes on their network., 17 pages, 17 figures. arXiv admin note: text overlap with arXiv:1804.04358

We introduce a new decentralized observation condition which we call "at least one can tell" (OCT) and which attempts to capture the idea that for any possible behavior that a system can generate, at least one decentralized observation agent can tell whether that behavior was "good" or "bad", for given formal specifications of "good" and "bad". We provide several equivalent formulations of the OCT condition, and we relate it to (and show that it is different from) previously introduced joint observability. In fact, contrary to joint observability which is undecidable, we show that the OCT condition is decidable. We also show that when the condition holds, finite-state decentralized observers exist.

We propose ε ↓ ( D → ) -logic as a formal foundation for the specification and development of event-based systems with data states. The framework is presented as an institution in the sense of Goguen and Burstall and the logic itself is parametrised by an underlying institution D → whose structures are used to model data states. ε ↓ ( D → ) -logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. It uses modal diamond and box operators over complex actions adopted from dynamic logic. Atomic actions are pairs [inline-graphic not available: see fulltext] where e is an event and ψ a state transition predicate capturing the allowed reactions to the event. To write concrete specifications of recursive process structures we integrate (control) state variables and binders of hybrid logic. The semantic interpretation relies on event/data transition systems. For the presentation of constructive specifications we propose operational event/data specifications allowing for familiar, diagrammatic representations by state transition graphs. We show that ε ↓ ( D → ) -logic is powerful enough to characterise the semantics of an operational specification by a single ε ↓ ( D → ) -sentence. Thus the whole (formal) development process for event/data-based systems relies on ε ↓ ( D → ) -logic and its semantics as a common basis. It is supported by a variety of implementation constructors which can express, among others, event refinement and parallel composition. Due to the genericity of the approach, it is also possible to change a data state institution during system development when needed. All steps of our formal treatment are illustrated by a running example.

In remote villages without access to modern IT technology, simple devices such as smartcards can be used to carry out business transactions. These devices typically store multiple business applications from multiple vendors. Although devices must prevent malicious or accidental security breaches among the applications, a secure communication channel between two applications from different vendors is often required. In this paper, first, we propose a method of establishing secure communication channels between applications in embedded operating systems that run on multi-applet smart cards. Second, we enforce the high assurance using an intransitive noninterference security policy. Thirdly, we formalize the method through the Z language and create the formal specification of the proposed secure system. Finally, we verify its correctness using Rushby's unwinding theorem.

This paper presents the experience of verifying server implementations of the TLS cryptographic protocol version 1.3. TLS is a widely used cryptographic protocol designed to create secure data transmission channels and provides the necessary functionality for this: confidentiality of the transmitted data, data integrity, and authentication of the parties. The new version 1.3 of the TLS protocol was introduced in August 2018 and has a number of significant differences compared to the previous version 1.2. A number of TLS developers have already included support for the latest version in their implementations. These circumstances make it relevant to do research in the field of verification and security of the new TLS protocol implementations. We used a new test suite for verifying implementations of the TLS 1.3 for compliance with Internet specifications, developed on the basis of the RFC8446, using UniTESK technology and mutation testing methods. The current work is part of the TLS 1.3 protocol verification project and covers some of the additional functionality and optional protocol extensions. To test implementations for compliance with formal specifications, UniTESK technology is used, which provides testing automation tools based on the use of finite state machines. The states of the system under test define the states of the state machine, and the test effects are the transitions of this machine. When performing a transition, the specified impact is passed to the implementation under test, after which the implementation's reactions are recorded and a verdict is automatically made on the compliance of the observed behavior with the specification. Mutational testing methods are used to detect non-standard behavior of the system under test by transmitting incorrect data. Some changes are made to the protocol exchange flow created in accordance with the specification: either the values of the message fields formed on the basis of the developed protocol model are changed, or the order of messages in the exchange flow is changed. The protocol model allows one to make changes to the data flow at any stage of the network exchange, which allows the test scenario to pass through all the significant states of the protocol and in each such state to test the implementation in accordance with the specified program. So far, several implementations have been found to deviate from the specification. The presented approach has proven effective in several of our projects when testing network protocols, providing detection of various deviations from the specification and other errors.

Editor’s notes: Controller synthesis using formal specifications has shown considerable promise in recent years. However, it is computationally very expensive. This article shows how cloud computing can come to the rescue. —Samarjit Chakraborty, University of North Carolina at Chapel Hill

Neural Networks are used today in numerous security- and safety-relevant domains and are, as such, a popular target of attacks that subvert their classification capabilities, by manipulating the network parameters. Prior work has introduced sensitive samples -- inputs highly sensitive to parameter changes -- to detect such manipulations, and proposed a gradient ascent-based approach to compute them. In this paper we offer an alternative, using symbolic constraint solvers. We model the network and a formal specification of a sensitive sample in the language of the solver and ask for a solution. This approach supports a rich class of queries, corresponding, for instance, to the presence of certain types of attacks. Unlike earlier techniques, our approach does not depend on convex search domains, or on the suitability of a starting point for the search. We address the performance limitations of constraint solvers by partitioning the search space for the solver, and exploring the partitions according to a balanced schedule that still retains completeness of the search. We demonstrate the impact of the use of solvers in terms of functionality and search efficiency, using a case study for the detection of Trojan attacks on Neural Networks., Comment: In Proceedings SCSS 2021, arXiv:2109.02501

In reactive synthesis, one begins with a temporal specification $$\varphi $$ φ , and automatically synthesizes a system $$M$$ M such that $$M\models \varphi $$ M ⊧ φ . As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system M satisfies $$\varphi $$ φ non-vacuously, then M is likely to be closer to the user’s intent, because it satisfies $$\varphi $$ φ in a more “meaningful” way. Narrowing the gap between the formal specification and the designer’s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.

How can the advantages of formal methods be brought to emerging smart cities? We discuss several core challenges and our recent efforts as the first step toward developing novel formal methods to ensure safety and performance in smart cities.

Performance portability is a critical issue for the Exascale Computing Project (ECP) because of nontrivial architectural differences between machines available today and those expected at exascale. Many ECP project teams are working toward performance portability, and would expect to benefit from sharing lessons learned, identifying gaps, and discovering opportunities for partnerships. To facilitate this communication, the IDEAS-ECP project partnered with the three focus areas of ECP (application development, software technology, and hardware and integration), and Department of Energy computing facilities, to lead a series of panel discussions on performance portability. The panels were organized around broadly common themes of algorithmic and data locality challenges. In this article, we describe the panel series, its objectives, and perspectives from the various areas of the project. We also discuss use cases that are distinctive, as well as conclusions drawn from the collective experience of the participants.

Symbolic execution is a powerful technique for automating software testing to detect many types of errors such as memory errors and assertion violations. However, it encounters the problem of path explosion, and by using only assertions, it still lacks the capability of going deep into checking the functional correctness of a path based on corresponding formal specifications. To address these problems, we propose a specification-based incremental testing method with symbolic execution, called SIT-SE, providing a much more rigorous way to automatically check the functional correctness of all the discovered program paths, by introducing theorems (instead of assertions) for path correctness and branch sequence coverage algorithm for guiding a moderate path exploration. Compared with Hoare logic for proving the correctness of an entire program, a theorem in the SIT-SE is made for verifying the correctness of a program path. The proposed method carefully treats the relationship between a path condition and the specification in a theorem to restrict the monotonous path exploration, whereas traditional concolic testing methods roughly use one test data to determine the path correctness by assertions during long path searching. We use a classic case to demonstrate how the method works and conduct an experiment to evaluate the performance of both the proposed method and the commonly used well-known concolic testing tool KLEE. The experimental results show that our method SIT-SE is effective and outperforms KLEE in detecting faulty paths based on specifications.

Active distribution network (ADN) technology, as an important trend of the future smart distribution grid, is able to effectively absorb distributed energy resource (DER), to reasonably optimise grid‐load operation characteristics, and to safely support the reliability of power supply. Through enhancing energy utilisation efficiency and friendly interaction with user access, ADN technology is also able to comprehensively improve the power supply reliability of the distribution network. However, distributed feeder automation (FA), as an important part of ADN technology, will also meet new problems and challenges with the access of DER in the distribution network. The formal method can analyse the correctness and effectiveness of a distributed fault processing algorithm from mathematical logic, which provides an important theoretical basis for distributed fault processing. The focus herein is on the formal description and verification of topology modelling in fault location, isolation, and service restoration (FLISR) based on distributed processing. By abstracting and simplifying the complex power system features, the adaptability of the formal method is solved. The logical correctness of the topology model in FLISR based on distributed processing is verified. Finally, the distributed local topology model and algorithm is verified through a formal method using an actual ADN example.

Digitalization changes products and their development. In this article, we investigate embedded and cyberphysical systems using the core technologies of the digital transformation and sketch out the skills that the next generation of requirements engineers must possess.

Engineering distributed self-adaptive systems is challenging due to multiple interacting components, some of which monitor and possibly modify the behavior of managed components that operate in highly dynamic settings. Formalizing such systems having a decentralized adaptation control has been recognized as a hard task. In this article, we introduce a formal framework based on Symmetric Nets (a well-established subclass of Colored Petri nets) for modeling and analyzing distributed self-adaptive discrete-event systems. Even though Petri Nets represent a sound and expressive formal model of concurrency and distribution, they cannot specify in a natural way structural changes enacted by adaptation procedures. We overcome this limitation by means of a two-layer modeling approach that enables clear separation of concerns and allows multiple decentralized adaptation procedures to be specified, validated, and verified against formal requirements. Validation and verification techniques are supported by powerful off-the-shelf tools tailored to Symmetric Nets. A self-healing manufacturing system case study is used to show applicability, advantages, and shortcomings of the approach. In particular, complexity issues are thoroughly discussed and mitigated by adopting complementary approaches based on interleaving reduction and behavioral symmetries exploitation.

Model-based design is now unavoidable when building embedded systems and, more specifically, controllers. Among the available model languages, the synchronous dataflow paradigm, as implemented in languages such as MATLAB Simulink or ANSYS SCADE, has become predominant in critical embedded system industries. Both of these frameworks are used to design the controller itself but also provide code generation means, enabling faster deployment to target and easier V&V activities performed earlier in the design process, at the model level. Synchronous models also ease the definition of formal specification through the use of synchronous observers, attaching requirements to the model in the very same language, mastered by engineers and tooled with simulation means or code generation. However, few works address the automatic synthesis of MATLAB Simulink annotations from lower-level models or code. This article presents a compilation process from Lustre models to genuine MATLAB Simulink, without the need to rely on external C functions or MATLAB functions. This translation is based on the modular compilation of Lustre to imperative code and preserves the hierarchy of the input Lustre model within the generated Simulink one. We implemented the approach and used it to validate a compilation toolchain, mapping Simulink to Lustre and then C, thanks to equivalence testing and checking. This backward compilation from Lustre to Simulink also provides the ability to produce automatically Simulink components modeling specification, proof arguments, or test cases coverage criteria.

IoT systems are required to manage themselves to changes regarding their internal and external contexts. So, adaptability is a very important aspect in IoT software systems. The MAPE (Monitoring, Analysis, Planning, Execution) control loop model, inspired from the autonomic nervous system, has been identified as a crucial element for realizing self-adaptation in software systems. In fact, software design patterns provide architects and developers with reusable software elements helping them to master building complex software systems including several interconnected components. Complex self-adaptive systems require several architectural patterns in their design which leads to the need of architectural pattern composition. In this paper, we focus in modeling adaptability in IoT systems through a set of MAPE design patterns for decentralized control in self-adaptive systems and we propose an approach for composing them using a UML profile. Then, we propose formalizing the composition process using the Event-B method. In addition, we propose verifying adaptation properties based on the resulting formal specification. We illustrate our approach by modeling structural and behavioral features of the hybrid pattern resulting from the composition of two MAPE patterns and applied to the fall-detection ambient assisting living system for elderly people.

A smart contract is a computer program that allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal, and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work. Energy Market Authority (EMA) Ministry of Education (MOE) National Research Foundation (NRF) This research is partially supported by the Ministry of Education, Singapore, under its Academic Research Fund Tier 1 (Award No. 2018-T1-002-069) and Tier 2 (Award No. MOE2018-T2-1-068), and by the National Research Foundation, Singapore, and the Energy Market Authority, under its Energy Programme (EP Award No. NRF2017EWT-EP003-023).

Software and systems engineering practitioners have the option to work with a very wide range of requirements specification methods. I view these as requirements languages. A subset of practitioners additionally has a compelling interest in using requirements methods that are suitable for very large-scale enterprise projects.1-4

Analyzing the behavior of sensors is becoming one of the key challenges due to their increasing use for decision making in IoT systems. The paper proposes an approach for a formal specification and analysis of such behavior starting from existing sensor traces. A model that embodies the sensor measurements over time in the form of stochastic automata is built, then temporal properties are fed to Statistical Model Checker to simulate the learned model and to perform analysis. LTL properties are employed to predict sensors’ readings in time and to check the conformity of sensed data with the sensor traces in order to detect any abnormal behavior. We also use LTL properties to analyze the collective behavior of a set of sensors and build a formal model that checks the conformity of a combination of sensors’ readings in time.

Presents papers from the 2020 IEEE Conference on Requirements Engineering and the ACM/ IEEE 23rd International Conference on Model Driven Engineering Languages and Systems (MODELS 2020).

The maturity of sensor network technologies has facilitated the emergence of an industrial Internet of Things (IIoT), which has collected an increasing volume of data. Converting these data into actionable intelligence for fault diagnosis is key to reducing unscheduled downtime and performance degradation, among other examples. This article formalizes a problem called semantic fault diagnosis— to construct the formal specifications of faults directly from data collected from IIoT-enabled systems. The specifications are written as signal temporal logic formulas, which can be easily interpreted by humans. To tackle the issue of the combinatorial explosion that arises, we propose an algorithm that combines ideas from agenda-based searching and imitation learning to train a policy that searches formulas in a strategic order. Specifically, we formulate the problem as a Markov decision process, which is further solved with a reinforcement learning algorithm. Our algorithm is applied to time-series data collected from an IIoT-enabled iron-making factory. The results show empirically that our proposed algorithm is both scalable to the size of the data set and interpretable, therefore allowing human users to take actions, for example, predictive maintenance.

The purpose of this research study is to look at, how the utilization of planning techniques / strategies having the most important impacts on any project /organization’s success and imaginative problem?solving. In particular Project Planning Techniques, three most important arranging basic strategies including, Gantt graphs, case?based arranging and basic way investigation, were studied &analyzed. As this study is an empirical in nature which purposes to highlight the project standards used to examine the accomplishment of projects and the project planning techniques being practically applicable. It is quantitative research study and questionnaires were asked to access the variables and associate with the existing literature. Project Success criteria were graded which were found to be dissimilar in this field as compare to others. It also presented the knowledge and usage of project planning techniques for categorizing the room of improvement as for as the Project Success is concerned, where some professional trainings are required for the project team members. The role of Effective Project Governance is also very vital for project success as well. The main focus and targeted area is the construction industry of Pakistan.

NoSQL solutions are started to be increasingly used in modern days’ Data Warehouses (DW). However, business analysts face challenges when performing On Line Analytical Processing (OLAP) queries on these NoSQL systems. The lack of uniform representation of various OLAP operations over different types of NoSQL based DWs is one of them. In addition, deficiency of precise semantics in OLAP operations create obstacles to effective query interpretation over distinct types DWs. This paper is aiming to deal with aforementioned challenges. Formal and rigorous specification are represented in this paper for different kinds of OLAP operators and operations. These precise specifications are capable to analyse business queries. Further, the proposed formal specifications are implemented in a document-oriented database using a suitable case study. In addition, the proposed approach aids efficient visualization techniques of data cubes over NoSQL based DWs.

In this paper, we present a process calculus called BigrTiMo that combines the rTiMo calculus and the Bigraph model. BigrTiMo calculus is capable of specifying a rich variety of properties for structure-aware mobile systems. Compared with rTiMo, our BigrTiMo calculus can specify not only time, mobility and local communication, but also remote communication. We then investigate the operational semantics of the BigrTiMo calculus and develop an executable formal specification of our BigrTiMo calculus in a declarative language called Maude. In addition, we verify safety properties and liveness properties of the mobile systems described by BigrTiMo using state exploration and LTL model checking in Maude. Based on Hoare and He's Unifying Theories of Programming (UTP), we study the semantic foundation of this highly expressive modelling language and propose a denotational semantic model and a set of algebraic laws for it. The semantic model in this paper covers time, location, communication and global shared variable at the same time. We also demonstrate the proofs of some algebraic laws based on our denotational semantics. Moreover, we explore how the algebraic semantics relates with the operational semantics and denotational semantics, which is conducted by the study of deriving the operational semantics and denotational semantics from algebraic semantics. We prove the equivalence between the derived transition system (e.g., the operational semantics) and the derivation strategy, which indicates that the operational semantics is sound and complete.

Modern software systems, either system or application software, are increasingly being developed on top of virtualized software platforms. They may simply intend to execute on virtual machines or they may be expected to port to physical machines eventually. In either case, the devices, virtual or silicon, in the target virtual or physical machines are expected to conform to the specifications based on which the software systems have been developed. Non-conformance of these devices to the specifications can cause catastrophic failures of the software systems. In this article, we propose a mutation-based framework for effective and efficient conformance checking between virtual/silicon device implementations and their specifications. Based on our defined mutation operators, device specifications can be automatically instrumented with weak mutant-killing constraints to model potential erroneous device behaviors. To kill all feasible mutants, our approach adopts a cooperative symbolic execution mechanism that can efficiently automate the test case generation and conformance checking for virtual/silicon devices. By symbolically executing the instrumented specifications with virtual/silicon device traces obtained from the cooperative execution, our method can accurately measure whether the designs have been sufficiently validated and report the inconsistencies between device specifications and implementations. Comprehensive experiments on two industrial network adapters and their virtual devices demonstrate the effectiveness of our proposed approach in conformance checking for both virtual and silicon devices.

Model checking has advanced over the last decades to become an effective formal technique for verifying distributed and concurrent systems. As computers grew in memory and processing capacity, it became possible to exhaustively verify systems with billions of states, making it practical to model and verify real-world protocols and algorithms. However, writing a model is a manual task that potentially introduces defects which the model checker tool finds to fulfill the formal specification (e.g., an incorrect model that fulfills an incomplete specification). Furthermore, this kind of formal verification technique is limited by the well-known state-space explosion problem. This paper aims to provide a set of generic template models, appropriate for distributed round-based algorithms, to be used to focus modeling effort on algorithm-specific details. To mitigate state-space explosion, the paper proposes two reduction techniques, named partition symmetry reduction and message order reduction, that exploit symmetries in the state space to avoid expanding equivalent states. The reusable framework for verifying round-based algorithms and the two proposed reduction techniques provide the means for reducing by orders of magnitude the number of states required to analyze common distributed algorithms.

The paper explores an approach aimed to formulate particular and generalized target functions for a formal specification of the problem of adaptive and optimal monitoring of integrated security in modern material processing systems and technologies. The formulation of the target functions is carried out taking into account the whole variety of factors affecting the procedures of observation, assessment and prediction within the conceptual model of adaptive monitoring. The stages of implementation of these target functions as a joint sequential dynamic adaptation of the parameters of observation, assessment and prediction procedures (i.e. monitoring parameters) of the integrated security state are proposed. Practical implementation of the proposed approach to the formalization of monitoring tasks will increase its effectiveness by improving the nonredundancy, reliability and accuracy of the state assessment and prediction of integrated security for material processing systems and technologies.

Model-based approaches are essential for designing cyber-physical systems, which adopt the formal models to simultaneously form the specifications and enable the verification at an early stage. Aimed to model the complex structure and continuous-discrete hybrid behavior of cyber-physical systems, this paper mathematically defines a dynamic relational system so that the cyber-physical system can be regarded as dynamic relational systems in a hierarchical structure and each dynamical relational system is a triple of dynamic attributes, subsystems, and hybrid relations between attributes and subsystems. Every hybrid relation contains a tuple and a predicate to govern the system behaviors. By utilizing the dynamic relational system, a parametric abstraction is then performed to specify the design requirements and schemes. It can represent the structure and behaviors of multiple cyber-physical system design schemes in an integrated manner. With a mathematical foundation, the constructed relational models are beneficial for structural analysis and behavior verification. An implementation case of a friction-driven plate conveyor is presented to illustrate the design specification with relational models, and the connectivity analysis and behavior verifications are carried out to show the effectiveness and engineering practicability of the achieved models.

Ensuring correctness of cyber-physical systems (CPS) is a challenging task that is in practice often addressed with simulation-based testing. Formal specification languages, such as Signal Temporal Logic (STL), are used to mathematically express CPS requirements and thus render the simulation activity more principled. We propose a novel method for adaptive generation of tests with specification coverage for STL. To achieve this goal, we devise cooperative reachability games that we combine with numerical optimization to create tests that explore the system in a way that exercise various parts of the specification. To the best of our knowledge our approach is the first adaptive testing approach that can be applied directly to MATLAB™ Simulink/Stateflow models. We implemented our approach in a prototype tool and evaluated it on several illustrating examples and a case study from the avionics domain, demonstrating the effectiveness of adaptive testing to (1) incrementally build a test case that reaches a test objective, (2) generate a test suite that increases the specification coverage, and (3) infer what part of the specification is actually implemented.

Recent years have seen an increasing use of Signal Temporal Logic (STL) as a formal specification language for symbolic control, due to its expressiveness and closeness to natural language. Furthermore, STL specifications can be encoded as cost functions using STL's robust semantics, transforming the synthesis problem into an optimization problem. Unfortunately, these cost functions are non-smooth and non-convex, and exact solutions using mixed-integer programming do not scale well. Recent work has focused on using smooth approximations of robustness, which enable faster gradient-based methods to find local maxima, at the expense of soundness and/or completeness. We propose a novel robustness approximation that is smooth everywhere, sound, and asymptotically complete. Our approach combines the benefits of existing approximations, while enabling an explicit tradeoff between conservativeness and completeness., Comment: Accepted to L-CSS

Nowadays, extended state machines are prominent requirements specification techniques due to their capabilities of modeling complex systems in a compact way. These machines extend the standard state machines with variables and have transitions guarded by enabling predicates and may include variable update statements. Given a system modeled as an extended state machine, with possibly infinite state space and some non-controllable (parameterized) interactions, a pruning procedure is proposed to symbolically derive a maximal sub-machine of the original system that satisfies certain conditions; namely, some safeness and absence of undesirable deadlocks which could be produced during pruning. In addition, the user may specify, as predicates associated with states, some general goal assertions that should be preserved in the obtained sub-machine. Further, one may also specify some specific requirements such as the elimination of certain undesirable deadlocks at states, or fail states that should never be reached. Application examples are given considering deadlock avoidance and loops including infinite loops over non-controllable interactions showing that the procedure may not terminate. In addition, the procedure is applied for finding a controller of a system to be controlled. The approach generalizes existing work in respect to the considered extended machine model and the possibility of user defined control objectives written as assertions at states.

Blockchain- and smart-contract technology enhance the effectiveness and automation of business processes. The rising interest in the development of decentralized autonomous organizations (DAO) shows that blockchain technology has the potential to reform business and society. A DAO is an organization wherein business rules are encoded in smart-contract programs that are executed when specified rules are met. The contractual- and business semantics are sine qua non for drafting a legally-binding smart contract in DAO collaborations. Several smart-contract languages (SCLs) exist, such as SPESC, or Symboleo to specify a legally-binding contract. However, their primary focus is on designing and developing smart contracts with the cooperation of IT- and non-IT users. Therefore, this paper fills a gap in the state of the art by specifying a smart-legal-contract markup language (SLCML) for legal- and business constructs to draft a legally-binding DAO. To achieve the paper objective, we first present a formal SCL ontology to describe the legal- and business semantics of a DAO. Secondly, we translate the SCL ontology into SLCML, for which we present the XML schema definition. We demonstrate and evaluate our SLCML language through the specification of a real life-inspired Sale-of-Goods contract. Finally, the SLCML use-case code is translated into Solidity to demonstrate its feasibility for blockchain platform implementations.

Technological advances and increasing customer need for highly customized products have triggered a fourth industrial revolution. A digital revolution in the manufacturing industry is enforced by introducing smart devices and knowledge bases to form intelligent manufacturing information systems. One of the goals of the digital revolution is to allow flexibility of smart factories by automating shop floor changes based on the changes in input production processes and ordered products. In order to make this possible, a formal language to describe production processes is needed, together with a code generator for its models and an engine to execute the code on smart devices. Existing process modeling languages are not usually tailored to model production processes, especially if models are needed for automatic code generation. In this paper we propose a research on Industry 4.0 manufacturing using a Domain-Specific Modeling Language (DSML) within a Model-Driven Software Development (MDSD) approach to model production processes. The models would be used to generate instructions to smart devices and human workers, and gather a feedback from them during the process execution. A pilot comparative analysis of three modeling languages that are commonly used for process modeling is given with the goal of identifying supported modeling concepts, good practices and usage patterns.

We consider Hoare-style verification for the graph programming language GP 2. In previous work, graph properties were specified by so-called E-conditions which extend nested graph conditions. However, this type of assertions is not easy to comprehend by programmers that are used to formal specifications in standard first-order logic. In this paper, we present an approach to verify GP 2 programs with a standard first-order logic. We show how to construct a strongest liberal postcondition with respect to a rule schema and a precondition. We then extend this construction to obtain strongest liberal postconditions for arbitrary loop-free programs. Compared with previous work, this allows to reason about a vastly generalised class of graph programs. In particular, many programs with nested loops can be verified with the new calculus., Comment: In Proceedings GCM 2020, arXiv:2012.01181. arXiv admin note: substantial text overlap with arXiv:2010.14549

The extent of formal verification methods applied to industrial projects has always been limited. The proliferation of distributed ledger systems (DLS), also known as blockchain, is rapidly changing the situation. Since the main area of DLSs' application is the automation of financial transactions, the properties of predictability and reliability are critical for implementing such systems. The actual behavior of the DLS is determined by the chosen consensus protocol, which properties require strict specification and formal verification. Formal specification and verification of the consensus protocol is necessary but not sufficient. It is required to ensure that the software implementation of the DLS nodes complies with this protocol. The verified software implementation of the protocol must run on a fairly reliable operating system. The so-called “smart contracts”, which are an important part of the applied implementations of specific business processes based on DLSs, must be verifiable as well. In this paper, we describe an ongoing industrial project that will result in a DLS verified at least at the four technological levels described above. We then share our experience with the formal specification and verification of HotStuff, a leader-based fault-tolerant protocol that ensures reaching distributed consensus in the presence of Byzantine processes.

Requirements prioritisation deals with the ranking or classification of user requirements based on their importance. This process is central to releasing a software product with features most favoured by users. While studies have explored the efforts that are dedicated to this cause, these tend to focus on a subset of the solutions that are available in the software engineering domain. Current techniques investigated in the software engineering domain do not consider the strengths inherent in requirements prioritisation techniques developed in other disciplines (e.g. product manufacturing), a gap that should be addressed. The authors thus conducted a comprehensive systematic mapping study and critical evaluation of studies that have provided implementations of requirements prioritisation techniques across multiple disciplines (including software engineering, product manufacturing, and engineering). Among their findings, they observed that while many solutions are targeted, quite often researchers have proposed solutions that were not evaluated. Most solutions were only validated as being operational, and the attributes studied had limited effects on performance outcomes. Their evidence suggests that new techniques may address the requirements prioritisation challenge if they are inspired by hybrid approaches developed across multiple disciplines. In addition, performance trade-offs are to be expected of such techniques, depending on their performance targets.

Reflex is a process-oriented language that provides a design of easy-to-maintain control software for programmable logic controllers. The language has been successfully used in a several reliability critical control systems, e. g. control software for a silicon single crystal growth furnace and electronic equipment control system. Currently, the main goal of the Reflex language project is to develop formal verification methods for Reflex programs in order to guarantee increased reliability of the software created on its basis. The paper presents the formal operational semantics of Reflex programs extended by annotations describing the formal specification of software requirements as a necessary basis for the application of such methods. A brief overview of the Reflex language is given and a simple example of its use – a control program for a hand dryer – is provided. The concepts of environment and variables shared with the environment are defined that allows to disengage from specific input/output ports. Types of annotations that specify restrictions on the values of the variables at program launch, restrictions on the environment (in particular, on the control object), invariants of the control cycle, pre- and postconditions of external functions used in Reflex programs are defined. Annotated Reflex also uses standard annotations assume, assert and havoc. The operational semantics of the annotated Reflex programs uses the global clock as well as the local clocks of separate processes, the time of which is measured in the number of iterations of the control cycle, to simulate time constraints on the execution of processes at certain states. It stores a complete history of changes of the values of shared variables for a more precise description of the time properties of the program and its environment. Semantics takes into account the infinity of the program execution cycle, the logic of process transition management from state to state and the interaction of processes with each other and with the environment. Extending the formal operational semantics of the Reflex language to annotations simplifies the proof of the correctness of the transformation approach to deductive verification of Reflex programs developed by the authors, transforming an annotated Reflex program to an annotated program in a very limited subset of the C language, by reducing a complex proof of preserving the truth of program requirements during the transformation to a simpler proof of equivalence of the original and the resulting annotated programs with respect to their operational semantics.

The development of systems with different features becomes increasingly challenging, given the actual context, implying on the search for new approaches for requirements elicitation. One of these approaches is design thinking (DT), a process of encouraging innovation used by designers, which presents itself as fundamental in the success of new products. This scenario motivates the importance of knowing DT concepts and their techniques, which can support requirements elicitation. In this context, the authors present DTA4RE (DT assistant for requirements elicitation), a tool that suggests DT techniques for requirements elicitation, which can be used by both students and professionals who would like to adopt DT in their projects. The DTA4RE is composed of a set of 27 techniques that could be suggested to the user through a recommendation questionnaire as well as an open repository with material to support the application of these techniques. Results from the authors’ two empirical studies with software engineering undergraduate and graduate students and industry professionals indicate that DTA4RE has helped in the selection of and in the learning of DT techniques when considering real problems. Most participants considered the questions from the recommendation questionnaire easy to answer, and the techniques suggested by the tool useful.

User-friendly formal specification and verification of concurrent and distributed systems for various domains, such as automatic control systems, telecommunications, and business processes, are active research topics due to their practical significance. In this paper, we present methods of developing verification-oriented domain-specific process ontologies used to describe concurrent systems of subject domains. One of the advantages of such ontologies is their formal semantics, which provides formal verification of the described systems. Our method is based on an abstract verification-oriented process ontology. We use two methods of domain specialization of the abstract process ontology. The declarative method relies on specializing classes of the original ontology, introducing new declarative classes, and using a new set of axioms to set restrictions on classes and relations of the abstract ontology. The constructive method uses semantic markup and pattern matching techniques to link domain concepts to classes of the abstract process ontology. We provide detailed ontological specifications for these techniques. Our methods preserve the formal semantics of the original process ontology; therefore, formal verification methods can be applied to the resulting domain-specific process ontologies. We demonstrate that the constructive method is a refined version of the declarative method. We illustrate our methods on the example of constructing an ontology for standard elements of automatic control systems: we develop declarative descriptions of the classes and restrictions of the domain-specific ontology in the Protege system in the Web Ontology Language (OWL) using inference rules written in the Semantic Web Rule Language (SWRL) and construct a system of semantic markup patterns that implements standard elements of automatic control systems.

With the development of blockchain technology, the fields of use of smart contracts are diversifying. Blockchain-based smart contracts are suitable in areas where integrity and transparency must be guaranteed with distributed ledger technology as the core. However, once the system is deployed, it cannot be modified, so it is important to ensure that the system works with the requirements and principles of the smart contract at the design stage. Therefore, in this paper, we aim to show that the system is accurate without contradictions/errors through formal verification using UPPAAL, a formal verification tool for the public descending auction system (Dutch Auction).

A Featured Transition System (FTS) models the behaviour of all products of a Software Product Line (SPL) in a single compact structure, by associating action-labelled transitions with features that condition their presence in product behaviour. It may however be the case that the resulting featured transitions of an FTS cannot be executed in any product (so called dead transitions) or, on the contrary, can be executed in all products (so called false optional transitions). Moreover, an FTS may contain states from which a transition can be executed only in some products (so called hidden deadlock states). It is useful to detect such ambiguities and signal them to the modeller, because dead transitions indicate an anomaly in the FTS that must be corrected, false optional transitions indicate a redundancy that may be removed, and hidden deadlocks should be made explicit in the FTS to improve the understanding of the model and to enable efficient verification—if the deadlocks in the products should not be remedied in the first place. We provide an algorithm to analyse an FTS for ambiguities and a means to transform an ambiguous FTS into an unambiguous one. The scope is twofold: an ambiguous model is typically undesired as it gives an unclear idea of the SPL and, moreover, an unambiguous FTS can efficiently be model checked. We empirically show the suitability of the algorithm by applying it to a number of benchmark SPL examples from the literature, and we show how this facilitates a kind of family-based model checking of a wide range of properties on FTSs.

QUIC is a new transport protocol combining the reliability and congestion control features of TCP with the security features of TLS. One of the main challenges with QUIC is to guarantee that any of its implementation follows the IETF specification. This challenge is particularly appealing as the specification is written in textual language, and hence may contain ambiguities. In a recent work, McMillan and Zuck proposed a formal representation of part of draft-18 of the IETF specification. They also showed that this representation made it possible to efficiently generate tests to stress four implementations of QUIC. Our first contribution is to complete and extend the formal representation from draft-18 to draft-29. Our second contribution is to test seven implementations of both QUIC client and server. Our last contribution is to show that our tool can highlight ambiguities in the QUIC specification, for which we suggest paths to corrections.

A formal specification of access control yields a deeper understanding of any operating system, and facilitates performing security analysis of the OS. In this paper, we provide a comprehensive formal specification of access control in Android (ACiA). Prior work is limited in scope, furthermore, recent developments in Android concerning dynamic runtime permissions require rethinking of its formalization. Our formal specification includes three parts, the user-initiated operations (UIOs) and app-initiated operations (AIOs) - which are distinguished based on the initiating entity, and the URI permissions which are utilized in sharing temporary access to data. We also studied the evolution of URI permissions from API 10 (Gingerbread) to API 22 (Lollipop), and a brief discussion on this is included in the paper. Formalizing ACiA allowed us to discover many peculiar behaviors pertaining to ACiA. In addition to that, we discovered two significant issues with permissions in Android which were reported to Google.