Search

We discuss integrating abstract data types (ADTs) in the KeY theorem prover by a new approach to model data types using Isabelle/HOL as an interactive back-end, and represent Isabelle theorems as user-defined taclets in KeY. As a case study of this new approach, we reason about Java’s interface using histories, and we prove the correctness of several clients that operate on multiple objects, thereby significantly improving the state-of-the-art of history-based reasoning. Open Science. Includes video material (Bian and Hiep in FigShare, 2021. https://doi.org/10.6084/m9.figshare.c.5413263) and a source code artifact (Bian et al. in Zenodo, 2022. https://doi.org/10.5281/zenodo.7079126).

Kalman filters are widely used for estimating the state of a system based on noisy or inaccurate sensor readings, for example in the control and navigation of vehicles or robots. However, numerical instability or modelling errors may lead to divergence of the filter, leading to erroneous estimations. Establishing robustness against such issues can be challenging. We propose novel formal verification techniques and software to perform a rigorous quantitative analysis of the effectiveness of Kalman filters. We present a general framework for modelling Kalman filter implementations operating on linear discrete-time stochastic systems, and techniques to systematically construct a Markov model of the filter's operation using truncation and discretisation of the stochastic noise model. Numerical stability and divergence properties are then verified using probabilistic model checking. We evaluate the scalability and accuracy of our approach on two distinct probabilistic kinematic models and four Kalman filter implementations.

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).

The notion of comparison between system runs is fundamental in formal verification. This concept is implicitly present in the verification of qualitative systems, and is more pronounced in the verification of quantitative systems. In this work, we identify a novel mode of comparison in quantitative systems: the online comparison of the aggregate values of two sequences of quantitative weights. This notion is embodied by comparator automata (comparators, in short), a new class of automata that read two infinite sequences of weights synchronously and relate their aggregate values. We show that aggregate functions that can be represented with B\"uchi automaton result in comparators that are finite-state and accept by the B\"uchi condition as well. Such $\omega$-regular comparators further lead to generic algorithms for a number of well-studied problems, including the quantitative inclusion and winning strategies in quantitative graph games with incomplete information, as well as related non-decision problems, such as obtaining a finite representation of all counterexamples in the quantitative inclusion problem. We study comparators for two aggregate functions: discounted-sum and limit-average. We prove that the discounted-sum comparator is $\omega$-regular iff the discount-factor is an integer. Not every aggregate function, however, has an $\omega$-regular comparator. Specifically, we show that the language of sequence-pairs for which limit-average aggregates exist is neither $\omega$-regular nor $\omega$-context-free. Given this result, we introduce the notion of prefix-average as a relaxation of limit-average aggregation, and show that it admits $\omega$-context-free comparators i.e. comparator automata expressed by B\"uchi pushdown automata.

Automated formal verification techniques, based on model checking and theorem proving, usually have scalability issues for contemporary digital circuits. On the other hand, interactive theorem provers can overcome this issue, by verifying circuits using universally quantified variables, at the cost of significant skilled guidance. Leveraging upon the complimentary nature of the techniques, this paper presents a hybrid model checking - theorem proving approach for the formal functional verification of digital circuits (HVoC). The main idea is to first use a higher-order-logic theorem prover to replace the structural (RTL or gate level) implementations of the combinational modules with their, formally verified, corresponding behavior and then verify the complete behavioral implementation using a model checker. This kind of a 2-step process not only reduces the computational complexity, but, is also quite effective in terms of counterexample generation time. Our experiments on some benchmarks show an average $$50\%$$ reduction in analysis time.

Computing reachability probabilities is a fundamental problem in the analysis of randomized programs. This article aims at a comprehensive and comparative account of various martingale-based methods for over- and under-approximating reachability probabilities. Based on the existing works that stretch across different communities (formal verification, control theory, etc.), we offer a unifying account. In particular, we emphasize the role of order-theoretic fixed points—a classic topic in computer science—in the analysis of randomized programs. This leads us to two new martingale-based techniques, too. We also make an experimental comparison using our implementation of template-based synthesis algorithms for those martingales.

The mutual exclusion protocol invented by Mellor-Crummey and Scott (called MCS protocol) is used to exemplify that state picture designs based on which the state machine graphical animation (SMGA) tool produces graphical animations should be better visualized. Variants of MCS protocol have been used in Java virtual machines and therefore the 2006 Edsger W. Dijkstra Prize in Distributed Computing went to their paper on MCS protocol. The new state picture design of a state machine formalizing MCS protocol is assessed based on Gestalt principles, more specifically proximity principle and similarity principle. We report on a core part of a formal verification case study in which the new state picture design and the SMGA tool largely contributed to the successful completion of the formal proof that MCS protocol enjoys the mutual exclusion property. The lessons learned acquired through our experiments are summarized as two groups of tips. The first group is some new tips on how to make state picture designs. The second one is some tips on how to conjecture state machine characteristics by using the SMGA tool. We also report on one more case study in which the state picture design has been made for the mutual exclusion protocol invented by Anderson (called Anderson protocol) and some characteristics of the protocol have been discovered based on the tips.

Refinement relations, such as trace containment, simulation preorder, and their alternating versions, have been successfully applied in formal verification of concurrent systems. Recently, trace containment and simulation preorder have been adopted and developed in fuzzy systems, but the generalization of their alternating versions to fuzzy systems has not been investigated. To satisfy the need for modeling and analyzing fuzzy systems, this article proposes two types of refinement relations called fuzzy alternating trace containment and fuzzy alternating simulation preorder, based on fuzzy concurrent game structures (FCGSs) under the Godel semantics. These two fuzzy notions inherit properties from the corresponding classical setting. For example, fuzzy alternating simulation preorder for finite-state FCGSs can be computed in polynomial time; fuzzy alternating simulation preorder is a fuzzy subset of fuzzy alternating trace containment, and both relations can be logically characterized in terms of fuzzy version of alternating-time temporal logic. These properties make the theory developed here suitable for the modeling and verification of fuzzy systems.

Cloud and Fog computing have been widely recognized as attractive solutions in both academic and industrial sectors. Despite their benefits, the adoption of Cloud and Fog computing still have considerable challenges to be handled due to the increase of client requirements. A crucial issue, in this context, is how to verify the correctness of Cloud and Fog systems. The use of formal methods is an efficient mean which provides a real help for the designer to evaluate the behaviour of a system and prevent errors before its implementation. In this paper, we present a systematic literature review (SLR) on the current state of the art in this field. We collect the existing studies on the use of formal methods for proving the correctness of Cloud and Fog systems. The proposed approaches are compared based on some technical properties such as the verification methods, the verification tools, the considered properties, and the application domains. In addition, future directions which need more investigations are presented. We believe that our paper will be useful for industry and academic researchers to understand the existing contributions that deal with the cor- rectness of Cloud and Fog systems. Moreover, it helps them to address several gaps in the literature.

Structural and behavioural properties of models are very important in development of complex systems and applications. In this paper, we investigate such properties for some classes of SN P systems. First, a class of SN P systems associated to a set of routing problems are investigated through their matrix representation. This allows to make certain connections amongst some of these problems. Secondly, the behavioural properties of these SN P systems are formally verified through a natural and direct mapping of these models into kP systems which are equipped with adequate formal verification methods and tools. Some examples are used to prove the effectiveness of the verification approach.

Safety is one of the most important features of modern software systems, especially safety-critical systems such as nuclear power plants, which can be checked exactly by model checking. Model checking is a formal verification technique that analyzes system properties through exploring all reachable states (state space) of a model of a system. The problem of the technique is that it confronts the state space explosion in large and complex systems due to exponential memory usage. Recent researches show that a partial and intelligent exploration of the state space can be a suitable solution to overcome this problem. In this paper, we propose a two-phase model checking for safety analysis of systems specified formally through graph transformations. In the first phase, the beam-search algorithm explores the state space to a specific number of states. In case of failure of the phase, the second phase starts: in systems specified through graph transformations, the rule applied on the previous state can determine the rule that can perform on the next state. In other words, the rule on current state depends on only the rule applied to previous state, not the one on earlier states. Hence, a Markov chain (MC) is estimated to capture dependencies between the sequence of applied rules in the state space explored by the beam-search algorithm. The MC is then employed to explore the remainder of the state space intelligently. To evaluate the effectiveness of the two-phase model checking, we implement it in GROOVE, an open source toolset for designing and model checking graph transformation systems. Experimental results show that the two-phase model checking has the high speed and accuracy in comparison with the existing meta-heuristic and evolutionary techniques.

Parity gamesare infinite-round two-player games played on directed graphs whose nodes are labeled with priorities. The winner of a play is determined by the smallest priority (even or odd) that is encountered infinitely often along the play. In the last two decades, several algorithms for solving parity games have been proposed and implemented in , a platform written in OCaml. includes theZielonka’s recursive algorithm(, for short) which is known to be the best performing one over random games. Notably, several attempts have been carried out with the aim of improving the performance of in , but with small advances in practice. In this work, we deeply revisit the implementation of by dealing with the use of specific data structures and programming languages such asScala,Java,C++, andGo. Our empirical evaluation shows that these choices are successful, gaining up to three orders of magnitude in running time over the classic version of the algorithm implemented in .

Building a trustworthy life-critical embedded system requires deep reasoning about the potential effects that sequences of machine instructions can have on full system operation. Rather than trying to analyze complete binaries and the countless ways their instructions can interact with one another — memory, side effects, control registers, implicit state, etc. — we explore a new approach. We propose an architecture controlled by a thin computational layer designed to tightly correspond with the lambda calculus, drawing on principles of functional programming to bring the assembly much closer to myriad reasoning frameworks, such as the Coq proof assistant. This approach allows assembly-level verified versions of critical code to operate safely in tandem with arbitrary code, including imperative and unverified system components, without the need for large supporting trusted computing bases. We demonstrate that this computational layer can be built in such a way as to simultaneously provide full programmability and compact, precise, and complete semantics, while still using hardware resources comparable to normal embedded systems. To demonstrate the practicality of this approach, our FPGA-implemented prototype runs an embedded medical application which monitors and treats life-threatening arrhythmias. Though the system integrates untrusted and imperative components, our architecture allows for the formal verification of multiple properties of the end-to-end system. We present a proof of correctness of the assembly-level implementation of the core algorithm in Coq, the integrity of trusted data via a non-interference proof, and a guarantee that our prototype meets critical timing requirements.

Reachability analysis is one of the most basic and challenging problems in verification. We investigate this problem in multi-agent reinforcement learning (MARL) system by transforming the reachability analysis to decision-making problem tackled by mixed integer linear programming (MILP) solver Gurobi. We define syntax and semantics for multi-role strategy logic (mrSL) which is used to describe the reachability specification. The logic mrSL is a variant of SL to express properties, which provide a holistic perspective to describe reachability properties instead of specifying a specific agent reaches a certain state in the MARL system. And the algorithms to translate reachability property into MILP constraints are provided. A tool called MAReachAnalysis is introduced, which uses Gurobi to solve the corresponding reachability problem and evaluate it on the predator-prey task of multi-agent deep deterministic policy gradient (MADDPG) example, discussion of the experimental results obtained on a range of test cases.

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.

The Automatic Dependent Surveillance-Broadcast (ADS-B) system allows aircraft to communicate current state information, including position and velocity messages, to other aircraft in their vicinity and to ground stations. The Compact Position Reporting (CPR) algorithm is the ADS-B protocol responsible for the encoding and decoding of aircraft positions. CPR is sensitive to computer arithmetic since it relies on functions that are intrinsically unstable such as floor and modulus. In this paper, a formal verification of the CPR algorithm is presented. In contrast to previous work, the algorithm presented here encompasses the entire range of message types supported by ADS-B. The paper also presents two implementations of the CPR algorithm, one in double-precision floating-point and one in 32-bit unsigned integers, which are both formally verified against the real-number algorithm. The verification proceeds in three steps. For each implementation, a version of CPR, which is simplified and manipulated to reduce numerical instability and leverage features of the datatypes, is proposed. Then, the Prototype Verification System (PVS) is used to formally prove real conformance properties, which assert that the ideal real-number counterpart of the improved algorithm is mathematically equivalent to the standard CPR definition. Finally, the static analyzer Frama-C is used to verify software conformance properties, which say that the software implementation of the improved algorithm is correct with respect to its idealized real-number counterpart. In concert, the two properties guarantee that the implementation meets the original specification. The two implementations will be included in the revised version of the ADS-B standards document as the reference implementation of the CPR algorithm.

Change of artefact-centric business process instances is important for an enterprise to keep competitive. However, to preserve the correctness of changes of an artefact-centric business process instance is still a big challenge. The hardness mainly stems from the fact that whether a business process instance can reach a final state has been proved to be undecidable. As such, finding a reliable verification algorithm for preserving correctness becomes impossible. In this study, the authors propose a random-forest-based approach to predict the correctness of changes in a business process instance. The availability of the proposed method is validated by comparing it to the traditional formal verification method. They also propose two optimisations of the proposed method and validate their effectiveness through extensive experimental analysis.

This study presents a formal description and verification method of the ontology transformation process of the distribution network information model based on the meta-model theory. By defining the dynamic change structures and model mapping constraints of the ontology transformation process of distribution network, a formalised specification for describing the key attributes of model updating and model mapping processes was constructed. The model updating and model mapping instances were specified using model checking verification tool SPIN. The method fundamentally guarantees the standardisation and reliability of the model ontology transformation process achieved by the meta-model.

In the context of disaster management, the intervention of Autonomous Systems brings many benefits to human rescuers. Autonomous Systems can quickly reach regions that may be inaccessible for humans. In addition, they can perform a rapid mapping of the impacted area and therefore enhancing the human knowledge. However, it is necessary to choose the best Autonomous Systems according to (i) mission environment and (ii) mission objectives. In this article, we describe our work on ArcTurius rover, a wheeled Autonomous System in support to disaster management. We validated its design through simulation and formal verification. A first simulation step occurs during the system definition. This allows to formally verify the design choices. A second type of simulation is performed to check the adequacy of the rover with respect to a specific mission. Thus, an Autonomous System can be adapted prior to a real mission to enhance its level of performance.

Camera pose estimation is key to the proper functioning of robotic systems, supporting critical tasks such as robot navigation, target tracking, camera calibration, etc.Whilemultiple algorithms solving this problem have been proposed, their correctness has rarely been validated using formal techniques. This is true despite the fact that the adoption of formal verification is essential for the reliability of safety-critical systems, and for their certification to high assurance levels. In this article, we present an effort in formally verifying an algorithm for camera pose estimation in an interactive theorem prover. The algorithm leverages the power of Rodrigues formula to solve the pose estimation problem under conditions for which existing solutions cannot be applied. The technical ingredients include (but are not limited to) mechanized proofs of the Rodrigues formula (along with its Cayley decomposition form) and the least squares method for fitting data. Based on the formalization of the algorithm, we formally derive and verify its general solution and unique solution.

Collaborative text editing systems allow multiple users to concurrently edit the same document, which can be modeled by a replicated list object. In the literature, there is a family of operational transformation (OT)-based Jupiter protocols for replicated lists, including AJupiter, XJupiter, and CJupiter. They are hard to understand due to the subtle OT technique, and little work has been done on formal verification of complete Jupiter protocols. Worse still, they use quite different data structures. It is unclear about how they are related to each other, and it would be laborious to verify each Jupiter protocol separately. In this work, we make contributions towards a better understanding of Jupiter protocols and the relation among them. We first identify the key OT issue in Jupiter and present a generic solution. We summarize several techniques for carrying out the solution, including the data structures to maintain OT results and to guide OTs. Then, we propose an implementation-independent AbsJupiter protocol. Finally, we establish the (data) refinement relation among these Jupiter protocols (AbsJupiter included). We also formally specify and verify the family of Jupiter protocols and the refinement relation among them using TLA+ (TLA stands for “Temporal Logic of Actions”) and the TLC model checker. To our knowledge, this is the first work to formally specify and verify a family of OT-based Jupiter protocols and the refinement relation among them. It would be helpful to promote a rigorous study of OT-based protocols.

Self-adaptive software (SAS) is gaining popularity as it can reconfigure itself in response to the dynamic changes in the operational context or itself. However, early modeling and formal analysis of SAS systems becomes increasingly difficult, as the system scale and complexity is rapidly increasing. To tackle the modeling difficulty of SAS systems, we present a refinement-based modeling and verification approach called EasyModel. EasyModel integrates the intuitive Unified Modeling Language (UML) model with the stepwise refinement Event-B model. Concretely, EasyModel: 1) creates a UML profile called AdaptML that provides an explicit description of SAS characteristics, 2) proposes a refinement modeling mechanism for SAS systems that can deal with system modeling complexity, 3) offers a model transformation approach and bridges the gap between the design model and the formal model of SAS systems, and 4) provides an efficient way to verify and guarantee the correct behaviour of SAS systems. To validate EasyModel, we present an example application and a subject-based experiment. The results demonstrate that EasyModel can effectively reduce the modeling and formal verification difficulty of SAS systems, and can incorporate the intuitive merit of UML and the correct-by-construction merit of Event-B.

Synthetic biology is an interdisciplinary field that uses well-established engineering principles for performing the analysis of the biological systems, such as biological circuits, pathways, controllers and enzymes. Conventionally, the analysis of these biological systems is performed using paper-and-pencil proofs and computer simulation methods. However, these methods cannot ensure accurate results due to their inherent limitations. Higher-order-logic (HOL) theorem proving is proposed and used as a complementary approach for analysing linear biological systems, which is based on developing a mathematical model of the genetic circuits and the bio-controllers used in synthetic biology based on HOL and analysing it using deductive reasoning in an interactive theorem prover. The involvement of the logic, mathematics and the deductive reasoning in this method ensures the accuracy of the analysis. It is proposed to model the continuous dynamics of the genetic circuits and their associated controllers using differential equations and perform their transfer function-based analysis using the Laplace transform in a theorem prover. For illustration, the genetic circuits of activated and repressed expressions and autoactivation of protein, and phase lag and lead controllers, which are widely used in cancer-cell identifiers and multi-input receptors for precise disease detection, are formally analyzed.

In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. Under consideration for acceptance in TPLP., Comment: Paper presented at the 36th International Conference on Logic Programming (ICLP 2019), University Of Calabria, Rende (CS), Italy, September 2020, 16 pages

Cell injection is an approach used for the delivery of small sample substances into a biological cell and is widely used in drug development, gene injection, intracytoplasmic sperm injection and in-vitro fertilization. Robotic cell injection systems provide the automation of the process as opposed to the manual and semi-automated cell injection systems, which require expert operators and involve time consuming processes and also have lower success rates. The automation of the cell injection process is obtained by controlling the orientation and movement of its various components, like injection manipulator, microscope etc., and planning the motion of the injection pipette by controlling the force of the injection. The conventional techniques to analyze the cell injection process include paper-and-pencil proof and computer simulation methods. However, both these techniques suffer from their inherent limitations, such as, proneness to human error for the former and the approximation of the mathematical expressions involved in the numerical algorithms for the latter. Formal methods have the capability to overcome these limitations and can provide an accurate analysis of these cell injection systems. Model checking, i.e., a state-based formal method, has been recently used for analyzing these systems. However, it involves the discretization of the differential equations capturing the continuous dynamics of the system and thus compromises on the completeness of the analysis of these safety-critical systems. In this paper, we propose a higher-order-logic theorem proving (a deductive-reasoning based formal method) based framework for analyzing the dynamical behavior of the robotic cell injection systems upto 4-DOF. The proposed analysis, based on the HOL Light theorem prover, enabled us to identify some discrepancies in the simulation and model checking based analysis of the same robotic cell injection system.

The Alternating-time Temporal Logic (ATL) is a temporal logic for formal verification of open systems, which supports selective quantification over paths. The open system can be represented as a game where the system and the environment pick their moves in turn or simultaneously. The ATL model checker Mocha has been developed by using Binary Decision Diagrams (BDDs), and successfully employed for open system verification. However, since Mocha symbolically manipulates a set of states by a BDD, it is hard to generate a winning strategy as a witness or a counter-example. In this paper, we propose a novel algorithm to efficiently construct a winning strategy tree and report that our technique has been successfully implemented on Mocha.

Despite the current increasing popularity of Behavior Trees (BTs) in the robotics community, there does not currently exist a method to formally verify their correctness without compromising their most valuable traits: modularity, flexibility and reusability. In this letter we present a new mathematical framework in which we formally express Behavior Trees in Linear Temporal Logic (LTL). We show how this framework equivalently represents classical BTs. Then we utilize the proposed framework to construct an algorithm to verify that a given BT satisfies a given LTL specification. We prove that this algorithm is sound. Importantly, we prove that this method does not compromise the flexible design process of BTs, i.e. changes to subtrees can be verified separately and their combination can be assured to be correct. We present an example of the proposed algorithm in use.

Parameterized model checking is a formal verification technique for verifying that some specifications hold in systems consisting of many similar cooperating but indistinguishable processes. The problem is known to be undecidable in general, even when restricted to reachability properties. To overcome this limitation, several techniques have been explored to address specific system families, logical formulas or topologies of process networks. Some use the notion of cutoff, i.e. if a certain property is verified for systems up to a certain size (the cutoff) then it is verified for systems of any size. Here we analyze the case of networks consisting of an arbitrary number of timed automata that can synchronize by looking at which state the neighbors are currently. We show that cutoffs exist independently from the checked formula, with or without a distinguished process acting as controller. We show how, exploiting the cutoffs, we can obtain upper bounds on complexity of the parameterized model-checking problem. Finally, we show how to use the theoretical results in order to model and verify a distributed algorithm for clock synchronization based on gossip techniques.

As a recently proposed membrane computing model, cP systems are capable of solving computational hard and distributed problems. Although several membrane system variants were formally verified in previous research, none of their approaches was applicable to cP systems. To formally verify the safety and liveness properties of cP systems, we solve a famous NP-Complete problem—the subset sum problem—in cP systems and use the PAT3 and ProB model checkers to verify the cP solution. Our cP solution outperforms previous work in time complexity and uses fewer rules. To perform model checking in cP systems, we define several mapping rules from cP notation to formal verification languages CSP# and B. We show that we can use model checkers to effectively detect design errors in cP systems. This work is the first study on formal verification of cP systems, and it showed that cP models can be effectively transformed into model checking problems and verified automatically.

This paper presents a methodology for the formal modeling of security attacks on cyber-physical systems, and the analysis of their effects on the system using logic theories. We consider attacks only on sensors and actuators. A simulated attack can be triggered internally by the simulation algorithm or interactively by the user, and the effect of the attack is a set of assignments to the variables defined in the Controller. The global effects of the attacks are studied by injecting attacks in the system model and co-simulating the overall system, including the system dynamics and the control part. Interesting properties of the behavior of the system under attack can also be formally proved by theorem proving. The INTO-CPS framework has been used for co-simulation, and the methodology is applied to the Line follower robot case study of the INTO-CPS project. The theorem prover of PVS has been used for deriving formal proofs of invariants of the system under attack.

In this work we propose a model checking approach to deal with the problem of the diagnosability verification. In this approach we consider the normal and the faulty behavior of a transition system (TS). We describe the diagnosability property by using an unique linear temporal logic (LTL) formula. Using LTL model checking we can test if the system is not diagnosable if it does not satisfy our proposed LTL-formula. Our approach can be carried out in SPIN model checker which is a tool used for formal verification of models. One advantage of SPIN is that it can handle a large state space which can be useful for diagnosability verification of complex system. We illustrate the effectiveness of our approach by means of a scalable benchmark of a railway level crossing system for n tracks and compare the results found with the ones found using typical tools for verification of diagnosability of Discrete Event Systems (DES).

Purpose Grid computing is an effective environment for the execution of parallel applications that requires great computing power. This paper aims to present, based on the hierarchical architecture, an improved weighted resource discovery (WRD) algorithm to manage allocation of resources and minimize cost of communications between grid nodes. Design/methodology/approach A behavioral modeling method is addressed to prove the proposed method correctness. The behavioral model of the proposed algorithm is implemented by StarUML tool with two different model-checking mechanisms. Then, the resource discovery correctness is analyzed in terms of reachability condition, fairness condition and deadlock-free using NuSMV model checker. Findings The results show that WRD algorithm has better performance in requiring re-discovery process, the number of examined nodes in each request and discovering the free resources with high-bandwidth links. Originality/value To store information of resources, a new data structure called resource information table is proposed which facilitates resource finding of the algorithm. A behavioral modeling method is addressed to prove the proposed method correctness.

Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification., Formal Methods in System Design, 54 (3), ISSN:0925-9856, ISSN:1572-8102

Nowadays, high-end Systems consist of thousands of individual devices which are in general heterogeneous. Grid computing environments are an example of high-end systems which are composed of many diverse and heterogeneous resources distributed within multiple geographical areas. The performance of such systems depends considerably on job scheduling and resource allocation algorithms. Indeed, to improve the global throughput of these environments, effective and efficient load balancing algorithms are fundamentally important. In this paper, we propose a completely distributed formal model for the description of grid architecture. Our model, is then parameterized to describe different job-scheduling algorithms in a completely parallel architecture. In particular, we focus on the modeling and description of distributed load-balancing algorithms. To reach this purpose, we define a set of parallel schedulers communicating together to achieve a given load-balancing policy. To show the applicability of our approach, we propose to specify and compare different well-known job-scheduling policies in grid environments. The formal verification of different properties of the studied protocols has been performed automatically using Model-checking and a set of performance analysis results are also provided.

International audience; EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical attackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL 2019). Leveraging our positive result, we implement EasyPQC, an extension of EasyCrypt for post-quantum security proofs, and use EasyPQC to verify postquantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption.

International audience; Complex systems and systems of systems (SoS) are systems characterized by the interconnection of a large number of components or subsystems. The complexity of such systems increases with the number of components and their manner of connectivity. The global behaviour of complex systems and SoS exhibits some properties that cannot be predicted by analysing components or subsystems in isolation. The verification of these properties called "emergent properties" is considered a crucial issue when engineering such systems. The purpose of this paper is to give an overview and verify emergent properties. In a first step, we have taken the blinker and the traffic light of the game of life as examples to verify emergence by using refinement techniques; in a second step, since the refinement is not straightforward, we have taken another example, the Boids model, and by using timed automata and UPPAAL model checking techniques, we have been able to simulate and verify emergent properties. Povzetek: Prispevek podaja pregled emergentnih lastnosti v kompleksnih sistemih.

Distributed systems have complex designs which are difficult to understand and verify. A rigorous specification of such systems using mathematical techniques such as formal methods is required to understand their precise behavior. Safety property implies that the system is free from deadlocks and safe with respect to the invariants, while the liveness property ensures that the system eventually makes progress. Various group communication protocols are one of the building blocks of reliable distributed systems applications. One of the message ordering protocols is the causal order broadcast in which message delivery at various processes takes places as per causal order. This paper presents how the liveness properties are preserved by message passing in causal order using Event-B. An incremental model for causal order-based message passing is constructed using Event-B specification. The properties of causal order broadcast are first specified using an abstract model, and then, details are added with each refinement step. Liveness property is ascertained by ensuring enabledness preservation and non-divergence among various refinements and is expressed as invariants in the model of causal order broadcast system.

A Featured Transition System (FTS) is a formalism for modeling variability in configurable system behavior. The behavior of all variants (products) is modeled in a single compact FTS by associating the possibility to perform an action and transition from one state to another with feature expressions that condition the execution of an action in specific variants. We present a front-end for the research tool VMC. The resulting toolchain allows a modeler to analyze an FTS for ambiguities (dead or false optional transitions and hidden deadlock states), transform an ambiguous FTS into an unambiguous one, and perform an efficient kind of family-based verification of an FTS without hidden deadlock states. We use benchmarks from the literature to demonstrate the novelties offered by the toolchain.

We present $\text{DY}^{\star}$ , a new formal verification framework for the symbolic security analysis of cryptographic protocol code written in the $\mathrm{F}^{\star}$ programming language. Unlike automated symbolic provers, our framework accounts for advanced protocol features like unbounded loops and mutable recursive data structures, as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. Our work extends a long line of research on using dependent type systems for this task, but takes a fundamentally new approach by explicitly modeling the global trace-based semantics within the framework, hence bridging the gap between trace-based and type-based protocol analyses. This approach enables us to uniformly, precisely, and soundly model, for the first time using dependent types, long-lived mutable protocol state, equational theories, fine-grained dynamic corruption, and trace-based security properties like forward secrecy and post-compromise security. $\text{DY}^{\star}$ is built as a library of $\mathrm{F}^{\star}$ modules that includes a model of low-level protocol execution, a Dolev-Yao symbolic attacker, and generic security abstractions and lemmas, all verified using $\mathrm{F}^{\star}$ . The library exposes a high-level API that facilitates succinct security proofs for protocol code. We demonstrate the effectiveness of this approach through a detailed symbolic security analysis of the Signal protocol that is based on an interoperable implementation of the protocol from prior work, and is the first mechanized proof of Signal to account for forward and post-compromise security over an unbounded number of protocol rounds.

We introduce a model for agent-environment systems where the agents are implemented via feed-forward ReLU neural networks and the environment is non-deterministic. We study the verification problem of such systems against CTL properties. We show that verifying these systems against reachability properties is undecidable. We introduce a bounded fragment of CTL, show its usefulness in identifying shallow bugs in the system, and prove that the verification problem against specifications in bounded CTL is in coNExpTime and PSpace-hard. We introduce sequential and parallel algorithms for MILP-based verification of agent-environment systems, present an implementation, and report the experimental results obtained against a variant of the VerticalCAS use-case and the frozen lake scenario.

The diversity of paths on the Internet makes it difficult for designers and operators to confidently deploy new congestion control algorithms (CCAs) without extensive real-world experiments, but such capabilities are not available to most of the networking community. And even when they are available, understanding why a CCA underperforms by trawling through massive amounts of statistical data from network connections is challenging. The history of congestion control is replete with many examples of surprising and unanticipated behaviors unseen in simulation but observed on real-world paths. In this paper, we propose initial steps toward modeling and improving our confidence in a CCA's behavior. We have developed CCAC, a tool that uses formal verification to establish certain properties of CCAs. It is able to prove hypotheses about CCAs or generate counterexamples for invalid hypotheses. With CCAC, a designer can not only gain greater confidence prior to deployment to avoid unpleasant surprises, but can also use the counterexamples to iteratively improvetheir algorithm. We have modeled additive-increase/multiplicative-decrease (AIMD), Copa, and BBR with CCAC, and describe some surprising results from the exercise.

Videogame level designs can contain errors called softlocks where a player traversing the level in an unintended manner can become permanently stuck. In this paper, we explore the automated detection of softlocks in the game Super Metroid using Computation Tree Logic (CTL). Super Metroid distinguishes itself as an example domain because of its velocity-based movement and rich item upgrade hierarchy. These factors can cause softlocks in Super Metroid to be challenging to detect visually. We contribute a tile-based gameplay abstraction for Super Metroid, and demonstrate verification of CTL properties for scenarios based on a segment of the original game’s level design. CTL can be used to define and test many other gameplay properties (e.g. which bosses can be skipped or which order items may be collected) and is immediately applicable to other game designs for which a compact abstraction of their state space can be enumerated. By making plausible design changes to a Super Metroid level fragment, we show how highly nonobvious softlocks can be detected and how the counterexamples resulting from verification failure can be turned into visualizations that explain the problem.

Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches have relied on techniques such as reachability relaxations, e.g., allowing for negative intermediate counter values. It is natural to question their feasibility for VASS enriched with primitives that typically translate into undecidability. Spurred by this concern, we pinpoint the complexity of integer relaxations with respect to arbitrary classes of affine operations. More specifically, we provide a trichotomy on the complexity of integer reachability in VASS extended with affine operations (affine VASS). Namely, we show that it is NP-complete for VASS with resets, PSPACE-complete for VASS with (pseudo-)transfers and VASS with (pseudo-)copies, and undecidable for any other class. We further present a dichotomy for standard reachability in affine VASS: it is decidable for VASS with permutations, and undecidable for any other class. This yields a complete and unified complexity landscape of reachability in affine VASS. We also consider the reachability problem parameterized by a fixed affine VASS, rather than a class, and we show that the complexity landscape is arbitrary in this setting.

Context-aware computing refers to system ability to sense its environment and modify its behavior for delivering suitable services. Having such kind of systems with the Near Field Communication (NFC) capability, opens new perspectives and research areas, allowing very useful type of applications known as NFC-based context-aware applications. These systems require correctness due to their applicability and then need to be proven formally using exhaustive analysis approach such as formal verification. In literature, most of works focuses on creating a general model for context aware systems ignoring the specificity of certain applications such as NFC applications where they present a higher complexity. We emphasize the existence of little or no work in this area supporting formal modeling. To boost it, we propose BigNFC as a novel formal-model based on Bigraphical Reactive Systems (BRS) taking account the interaction mode from the beginning, so we establish mapping between BRS and BigNFC components, where the structures are modelled as bigraphs and behaviors as rewriting rules. Finally, to validate our model, we have applied it on a real-life application and some properties were checked successfully.

International audience; We investigate three particular instances of the marking coverability problem in ordinary, safe Petri nets: the Dead Places Problem, the Dead Transitions Problem, and the Concurrent Places Problem. To address these three problems, which are of practical interest, although not yet supported by mainstream Petri net tools, we propose a combination of static and dynamic algorithms. We implemented these algorithms and applied them to a large collection of 13,000+ Petri nets obtained from realistic systems-including all the safe benchmarks of the Model Checking Contest. Experimental results show that 95% of the problems can be solved in a few minutes using the proposed approaches.