Formal Methods are mathematically-based techniques for software design and engineering, which enable the unambiguous description of and reasoning about a system's behaviour. Autonomous systems use software to make decisions without human control, are often embedded in a robotic system, are often safety-critical, and are increasingly being introduced into everyday settings. Autonomous systems need robust development and verification methods, but formal methods practitioners are often asked: Why use Formal Methods for Autonomous Systems? To answer this question, this position paper describes five recipes for formally verifying aspects of an autonomous system, collected from the literature. The recipes are examples of how Formal Methods can be an effective tool for the development and verification of autonomous systems. During design, they enable unambiguous description of requirements; in development, formal specifications can be verified against requirements; software components may be synthesised from verified specifications; and behaviour can be monitored at runtime and compared to its original specification. Modern Formal Methods often include highly automated tool support, which enables exhaustive checking of a system's state space. This paper argues that Formal Methods are a powerful tool for the repertoire of development techniques for safe autonomous systems, alongside other robust software engineering techniques.
Software model checking has experienced significant progress in the last two decades, however, one of its major bottlenecks for practical applications remains its scalability and adaptability. Here, we describe an approach to integrate software model checking techniques into the DevOps culture by exploiting practices such as continuous integration and regression tests. In particular, our proposed approach looks at the modifications to the software system since its last verification, and submits them to a continuous formal verification process, guided by a set of regression test cases. Our visi…
In industrial model-based development (MBD) frameworks, requirements are typically specified informally using textual descriptions. To enable the application of formal methods, these specifications need to be formalized in the input languages of all formal tools that should be applied to analyse the models at different development levels. In this paper we propose a unified approach for the computer-assisted formal specification of requirements and their fully automated translation into the specification languages of different verification tools. We consider a two-stage MBD scenario where first…
Autonomous robotic systems are complex, hybrid, and often safety-critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or provide sufficient evidence for the certification of, autonomous robotics. Formal methods for autonomous robotics have received some attention in the literature, but no resource provides a current overview. This short paper summarises the contributions of Luckcuck 2019, which surveys the state-of-the-art in formal specification and verification …
Automated Vehicles (AVs) are rapidly maturing in the transportation domain. However, the complexity of the AV design problem is such that no single technique is sufficient to provide adequate validation of key properties such as safety, reliability or trustworthiness. In this vision paper, a combination of a spatial traffic logic and agent-based verification methods with a validation method that uses assertion checking of simulations is proposed. We sketch how to integrate the respective approaches within a methodological framework called Corroborative Verification and Validation (V&V).The Cor…
Separation kernels are fundamental software of safety and security-critical systems, which provide to their hosted applications spatial and temporal separation as well as controlled information flows among partitions. The application of separation kernels in critical domain demands the correctness of the kernel by formal verification. To the best of our knowledge, there is no survey paper on this topic. This paper presents an overview of formal specification and verification of separation kernels. We first present the background including the concept of separation kernel and the comparisons am…
The work concerns automatic generation of logical specifications from requirements models. Logical specifications obtained in such a way can be subjected to formal verification using deductive reasoning. Formal verification concerns correctness of a model behaviour. Reliability of the requirements engineering is essential for all phases of software development processes. Deductive reasoning is an important alternative among other formal methods. However, logical specifications, considered as sets of temporal logic formulas, are difficult to specify manually by inexperienced users and this fact…
Verification of complex, safety-critical systems is a significant challenge. Manual testing and simulations are often used, but are only capable of exploring a subset of the system's reachable states. Formal methods are mathematically-based techniques for the specification and development of software, which can provide proofs of properties and exhaustive checks over a system's state space. In this paper, we present a formal requirements-driven methodology, applied to a model of an aircraft engine controller that has been provided by our industrial partner. Our methodology begins by formalising…
Formal methods yet advantageous, face challenges towards wide acceptance and adoption in software development practices. The major reason being presumed complexity. The issue can be addressed by academia with a thoughtful plan of teaching and practise. The user study detailed in this paper is examining AutoProof tool with the motivation to identify complexities attributed to formal methods. Participants' (students of Masters program in Computer Science) performance and feedback on the experience with formal methods assisted us in extracting specific problem areas that effect tool usability. Th…
Message Sequence Charts (MSCs) are an appealing visual formalism mainly used in the early stages of system design to capture the system requirements. However, if we move towards an implementation, an executable specifications related in some fashion to the MSC-based requirements must be obtained. The MSCs can be used effectively to specify the bus protocol in the way where high-level transition systems is used to capture the control flow of the system components of the protocol and MSCs to describe the non-atomic component interactions. This system of specification is amenable to formal verifi…
Events in the Solidity language provide a means of communication between the on-chain services of decentralized applications and the users of those services. Events are commonly used as an abstraction of contract execution that is relevant from the users' perspective. Users must, therefore, be able to understand the meaning and trust the validity of the emitted events. This paper presents a source-level approach for the formal specification and verification of Solidity contracts with the primary focus on events. Our approach allows specification of events in terms of the on-chain data that the…
How to apply automated verification technology such as model checking and static program analysis to millions of lines of embedded C/C++ code? How to package this technology in a way that it can be used by software developers and engineers, who might have no background in formal verification? And how to convince business managers to actually pay for such a software? This work addresses a number of those questions. Based on our own experience on developing and distributing the Goanna source code analyzer for detecting software bugs and security vulnerabilities in C/C++ code, we explain the unde…
In this paper, we present our ongoing work and initial results on the formal specification and verification of MiniMaple (a substantial subset of Maple with slight extensions) programs. The main goal of our work is to find behavioral errors in such programs w.r.t. their specifications by static analysis. This task is more complex for widely used computer algebra languages like Maple as these are fundamentally different from classical languages: they support non-standard types of objects such as symbols, unevaluated expressions and polynomials and require abstract computer algebraic concepts an…
Current approaches for the discovery, specification, and provision of services ignore the relationship between the service contract and the conditions in which the service can guarantee its contract. Moreover, they do not use formal methods for specifying services, contracts, and compositions. Without a formal basis it is not possible to justify through formal verification the correctness conditions for service compositions and the satisfaction of contractual obligations in service provisions. We remedy this situation in this paper. We present a formal definition of services with context-depen…
This paper presents an approach based on the analysis, design, and formal verification of a multi-agent based university Information Management System (IMS). University IMS accesses information, creates reports and facilitates teachers as well as students. An orchestrator agent manages the coordination between all agents. It also manages the database connectivity for the whole system. The proposed IMS is based on BDI agent architecture, which models the system based on belief, desire, and intentions. The correctness properties of safety and liveness are specified by First-order predicate logic…
A smart contract is a computer program which 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 presen…
Context: The complexity of modern safety-critical systems in industries keep on increasing due to the rising number of features and functionalities. This calls for formal methods in order to entrust confidence in such systems. Nevertheless, using formal methods in industry is demanding because of usability issues, e.g., the difficulty of understanding model checking results. Thus the hypothesis is, presenting the result of model checker results in a user-friendly manner could promote formal methods usage in industries. Objective: We aim to evaluate the acceptance of formal methods by engineers…
During the project of a communication protocol, many design decisions influence the behavior of the protocol and its correctness. Formal specification and verification of the protocol may prove its correctness. In this paper, an example of a verification of design decision using formal specification in CSM automata and verification in temporal logic is presented.
One of the most challenging tasks in software specifications engineering for a multi-agent system is to ensure correctness. As these systems have high concurrency, often have dynamic environments, the formal specification and verification of these systems along with step-wise refinement from abstract to concrete concepts play major role in system correctness. Our objectives are the formal specification, analysis with respect to functional as well as non-functional properties by step-wise refinement from abstract to concrete specifications and then formal verification of these specifications. A…
Formal analysis of functional and non-functional requirements is crucial in automotive systems. The behaviors of those systems often rely on complex dynamics as well as on stochastic behaviors. We have proposed a probabilistic extension of Clock Constraint Specification Language, called PrCCSL,for specification of (non)-functional requirements and proved the correctness of requirements by mapping the semantics of the specifications into UPPAAL models. Previous work is extended in this paper by including an extension of PrCCSL, called PrCCSL*, for specification of stochastic and dynamic system …
Development of quality assured software-intensive systems, such as automotive embedded systems, is an increasing challenge as the complexity of these systems significantly increases. EAST-ADL is an architecture description language developed to specify automotive embedded system architectures at multiple abstraction levels in the development of safety-critical automotive products. In this paper, we propose an architecture-based verification technique which enhances the model-based development process supported by EAST-ADL by adapting model-checking to EAST-ADL specifications. We employ UPPAAL …
The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the new autonomous behaviors of the vehicles in these platoons must be certified. An appropriate representation for vehicle platooning is as a multi-agent system in which each agent captures the "autonomous decisions" carried out by each vehicle. In order to ensure that these autonomous decision-making agents in vehicle platoons never violate safety requirements, we use formal verification. However, as the formal verification t…
Formal software verification uses mathematical techniques to establish that software has certain properties. For example, that the behaviour of a software system satisfies certain logically-specified properties. Formal methods have a long history, but a recurring assumption is that the properties to be verified are known, or provided as part of the requirements elicitation process. This working note considers the question: where do the verification properties come from? It proposes a process for systematically identifying verification properties.
The theory of actual causality, defined by Halpern and Pearl, and its quantitative measure - the degree of responsibility - was shown to be extremely useful in various areas of computer science due to a good match between the results it produces and our intuition. In this paper, I describe the applications of causality to formal verification, namely, explanation of counterexamples, refinement of coverage metrics, and symbolic trajectory evaluation. I also briefly discuss recent applications of causality to legal reasoning.
Model-Based Systems Engineering (MBSE) is a development approach aiming to build correct-by-construction systems, provided the use of clear, unambiguous and complete models to describe them along the design process. The approach is supported by several engineering tools that automate the development steps, for example the production of code, documentation, test cases and more. TASTE [1] is pragmatic MBSE toolset supported by ESA that encapsulates several technologies to design a system (data modelling, architecture modelling, behaviour modelling/implementation), to automatically generate the b…
MIT-IBM Watson AI Lab（MIT-IBM沃森人工智能实验室）；IBM Research（IBM研究院）；Massachusetts Institute of Technology（麻省理工学院）
Autonomous systems -- such as self-driving cars, autonomous drones, and automated trains -- must come with strong safety guarantees. Over the past decade, techniques based on formal methods have enjoyed some success in providing strong correctness guarantees for large software systems including operating system kernels, cryptographic protocols, and control software for drones. These successes suggest it might be possible to ensure the safety of autonomous systems by constructing formal, computer-checked correctness proofs. This paper identifies three assumptions underlying existing formal veri…
Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering
Lancaster University（兰卡斯特大学）；Tsinghua University（清华大学）；Harbin Institute of Technology（哈尔滨工业大学）；Southwest University（西南大学）；Aarhus University（奥胡斯大学）；University of York（约克大学）
IRISA（法国国家信息与自动化研究所布列塔尼大西洋分部）；University of South Brittany（南布列塔尼大学）；The Islamia University of Bahawalpur（巴哈瓦尔布尔伊斯兰大学）
It is important to have multi-agent robotic system specifications that ensure correctness properties of safety and liveness. As these systems have concurrency, and often have dynamic environment, the formal specification and verification of these systems along with step-wise refinement from abstract to concrete concepts play a major role in system correctness. Formal verification is used for exhaustive investigation of the system space thus ensuring that undetected failures in the behavior are excluded. We construct the system incrementally from subcomponents, based on software architecture. T…
DafnyBench: A Benchmark for Formal Software Verification
Harvard College（哈佛学院）；Massachusetts Institute of Technology（麻省理工学院）；Northeastern University（东北大学）；Stanford University（斯坦福大学）；University of California Irvine（加州大学欧文分校）；Harvard University（哈佛大学）
