Advances in automated theorem provers over the last decade have led to a renaissance in software tools that compile problems of correctness to problems over logic formula. In this talk, I will review progress in automated theorem provers, such as Z3 from Microsoft Research, and consider a variety of program correctness tools that build upon Z3, such as automated test generators, automated safety/termination checkers, as well as interactive functional verifiers. I'll then describe a number of new projects that make use of the "correctness via compilation to logic" approach, including the design of new programming languages, ensuring the security of data centers, and safely programming gesture recognizers such as Kinect.
Correct design, and system-level dependability prediction of highly-integrated systems demand the collocation of requirements and architectural artifacts within an integrated development environment. Hybrid systems, having dependencies and extensive interactions between their control portion and their environment, further intensify this need. AADL is a model-based engineering language for the architectural design and analysis of embedded control systems. Core AADL has been extended with a mechanism for discrete behavioral modeling and analysis of control systems, but not for the continuous behavior of the physical environment. In this paper, we introduce a lightweight language extension to AADL called the Hybrid Annex for continuous-time modeling, fulfilling the need for integrated modeling of the computing system along with its physical environment in their respective domains. The Isolette system described in the FAA Requirement Engineering Management Handbook is used to illustrate continuous behavior modeling with the proposed Hybrid Annex.
Ada 95, aka Ada9X at the time because we didn't know when we would be done, was a labor of love for most of us. A spectacular team was assembled from all over the world. I had the distinct pleasure and honor of being the Department of Defense Ada 9X Project Manager. The lessons I learned and the experience I gained allowed me to do many other things after Ada 95 was completed. I ran an Air Force space technology laboratory. I was responsible for building military satellites and launching them from the Cape. Currently, I am responsible for developing and operating the first purpose-built commercial spaceport. Looking back, the common thread through all of these endeavors is innovation, dedication, strong team work, and a passion for the job at hand. That can do spirit and boundless energy is a must for success and I have been fortunate to work on unprecedented projects with colleagues who possessed these qualities. Anecdotes from the Ada9X Project to today's emerging commercial space industry will be provided from my experiences and observations.
Specification based on Floyd-Hoare logic, using pre- and post-conditions, is common in languages aimed at high integrity software. Such pre/postcondition specifications are geared towards verification of code. While this specification technique has proven quite successful in the past 40 years, it has limitations when applied to API specification, particularly specification of generic interfaces. API-oriented design and genericity is of particular importance in modern large-scale software development. In this situation, algebraic specification techniques have a significant advantage. Unlike pre/post-based specification, which deals with the inputs and outputs of one operation at a time, algebraic specification deals with the relationships between the different operations in an API, which is needed in the specification of generic APIs.
Arguments about the safety, security, and correctness of a complex system are often made in the form of an assurance case. An assurance case is a structured argument, often represented with a graphical interface, that presents and supports claims about a system's behavior. The argument may combine different kinds of evidence to justify its top level claim. While assurance cases deliver some level of guarantee of a system's correctness, they lack the rigor that proofs from formal methods typically provide. Furthermore, changes in the structure of a model during development may result in inconsistencies between a design and its assurance case. Our solution is a framework for automatically generating assurance cases based on 1) a system model specified in an architectural design language, 2) a set of logical rules expressed in a domain specific language that we have developed, and 3) the results of other formal analyses that have been run on the model. We argue that the rigor of these automatically generated assurance cases exceeds those of traditional assurance case arguments because of their more formal logical foundation and direct connection to the architectural model.
This paper formally expresses the timing behavior of a cardiac pacemaker as defined in the PACEMAKER System Specification as understood by its principal author. The PACEMAKER System Specification was publicly released by Boston Scientific to provide a real-world subject for application of formal methods in response to Jim Woodcock's request at FM2006 for an industrial Grand Challenge problem. PACEMAKER's use for purposes other than formal methods has been surprising in its variety. Most ambitious is the Software Certification Consortium's mock regulatory submission, PACEMAKER Grand Challenge, to show that a product with safety-critical software is in fact safe. McMaster University is designing a second-generation hardware platform to execute formally-verified software during system feature test validation with an electrical heart simulator to show correct behavior. This paper uses first-order predicates, extended with a simple temporal operator, to formally express what the principal author understands to be "correct" behavior defined in PACEMAKER.
Modeling of Distributed Real-time Embedded systems using Architecture Description Language provides the foundations for various levels of analysis: scheduling, reliability, consistency, etc.; but also allows for automatic code generation. A challenge is to demonstrate that generated code matches quality required for safety-critical systems. In the scope of the AADL, the Ocarina toolchain proposes code generation towards the Ada Ravenscar profile with restrictions for High-Integrity. It has been extensively used in the space domain as part of the TASTE project within the European Space Agency. In this paper, we illustrate how the combined use of Ada 2012 and SPARK 2014 significantly increases code quality and exhibits absence of run-time errors at both run-time and generated code levels.
Complex asynchronous, distributed systems could benefit significantly from model checking, but model checking programs do not natively support verification of distributed software. Several frameworks have been developed recently that apply model checking to networked software, but none of these frameworks support complete modeling of programs that use the User Datagram Protocol (UDP). This paper presents the first framework to model realistic rather than ideal UDP network operations using Java Pathfinder, and describes its use in verifying a distributed UDP-based application.
To most in the software community, "modeling" is drawing pictures, something much different than "coding". While programming languages must be specified precisely enough to be executable, this has not necessarily been the case for modeling languages. Indeed, the well-known Unified Modeling Language (UML) has for years had a specification that is far from precise. However, precise models are quite common in other engineering disciplines, and there has been a minority even in software engineering that have created models that are precise enough to be, themselves, executable. Over the last decade, the UML community has more generally come to realize the benefits of having at least a subset of UML specified with precise execution semantics. While not all models need to be executable, executable models can support early testing and analysis of the design of critical software systems, as well as supporting simulation for communities using UML for modeling beyond just software (such as SysML for systems engineering). As a result, there has been a great deal of work in recent years toward the standardization of precise, executable semantics for UML models - the "meaning" behind the pictures: Foundational UML (fUML), the Action Language for fUML (Alf) and the recently completed Precise Semantics for UML Composite Structures. These new specifications provide the promise of widespread support for executable modeling across the many UML tools now on the market.
SPARK offers a way to develop formally-verified software in a language (Ada) that is designed with safety in mind and is further restricted by the SPARK language subset. However, much critical embedded software is developed in C or C++. We look at whether and how benefits similar to those offered by the SPARK language subset and associated tools can be brought to a C++ development environment.
Mission and safety critical software-reliant systems, aka. Cyber-physical systems, face the increasing challenges of exponential increase in verification related software rework cost. Industry studies show that 70% of defects are introduced in requirements and architecture design, while 80% are discovered post-unit test. The Architecture Analysis & Design Language (AADL) standard was targeted to address these issues through virtual system integration to analytically discover these system level issues regarding operational system properties early in the life cycle. After a summary of the challenges, the presentation highlights the expressive, analytical, and auto-generation capabilities of the AADL core language as well as several of its standardized extensions. The presentation then illustrates the importance of the analytical virtual system integration capabilities on several realistic industrial examples. In this context we discuss the benefit of well-defined semantics of nominal and fault behavior, timing, semantics of the model in AADL over other MBD notations. The presentation concludes by outlining a four part improvement strategy: architecture-led requirement specification to improve the quality of requirements, architecture refinement and incremental virtual system integration to discover issues early, compositional verification through static analysis to address scalability, and incremental verification and testing throughout the life cycle as assurance evidence.
The C programming language is widely used for programming space flight software and other safety-critical real time systems. C, however, is far from ideal for this purpose: as is well known, it is both low-level and unsafe. This paper describes Spot, a language derived from C for programming space flight systems. Spot aims to maintain compatibility with existing C code while improving the language and supporting verification with the SPIN model checker. The major features of Spot include actor-based concurrency, distributed state with message passing and transactional updates, and annotations for testing and verification. Spot also supports domain-specific annotations for managing spacecraft state, e.g., communicating telemetry information to the ground. We describe the motivation and design rationale for Spot, give an overview of the design, provide examples of Spot's capabilities, and discuss the current status of the implementation.
The increased presence of parallel computing platforms brings concerns to the general purpose domain that were previously prevalent only in the specific niche of high-performance computing. As parallel programming technologies become more prevalent in the form of new emerging programming languages and extensions of existing languages, additional safety concerns arise as part of the paradigm shift from sequential to parallel behaviour. In this paper, we propose various syntax extensions to the Ada language, which provide mechanisms whereby the compiler is given the necessary semantic information to enable the implicit and explicit parallelization of code. The model is based on earlier work, which separates parallelism specification from concurrency implementation, but proposes an updated syntax with additional mechanisms to facilitate the development of safer parallel programs.
This panel brings together designers of both traditional programming languages, and designers of behavioral specification languages for modeling systems, in each case with a concern for the challenges of multicore programming. Furthermore, several of these efforts have attempted to provide data-race-free programming models, so that multicore programmers need not be faced with the added burden of trying to debug race conditions on top of the existing challenges of building reliable systems.
In this industrial presentation we will demonstrate mbeddr, an extensible set of integrated languages for embedded software development. After discussing the context of the talk, we will give details about the mbeddr architecture, which relies on the MPS language workbench. Then we will elaborate on the extension modules and show how they fit with safety-critical development processes. Finally we will point out how the existing languages can be extended by the user by giving some real-world examples, including a language construct that could have prevented the Apple 'goto fail' bug as well as mathematical notations.
Rust is a new programming language for developing reliable and efficient systems. It is designed to support concurrency and parallelism in building applications and libraries that take full advantage of modern hardware. Rust's static type system is safe 1 and expressive and provides strong guarantees about isolation, concurrency, and memory safety. Rust also offers a clear performance model, making it easier to predict and reason about program efficiency. One important way it accomplishes this is by allowing fine-grained control over memory representations, with direct support for stack allocation and contiguous record storage. The language balances such controls with the absolute requirement for safety: Rust's type system and runtime guarantee the absence of data races, buffer overflows, stack overflows, and accesses to uninitialized or deallocated memory.
This presentation will comprise a discussion between two language designers, John Barnes and Tucker Taft, who have been intimately involved with the design of Ada over the past 30 years. During the discussion they will review the successful and less than completely successful features of the various versions of Ada, going from the original Ada 83, through the latest Ada 2012 version, and will attempt to identify some lessons to be learned about programming language design and evolution.
This tutorial will introduce the attendees to analysis and proof techniques for programs using parallelism and multi-threading. There are no specific prerequisites, but a familiarity with the notions of preconditions and postconditions, aliasing, race conditions, and deadlocks would be of value. The examples will be based on the threading and parallelism models of Java, Ada, and two new parallel languages, one called ParaSail [4] and another, inspired by the verifiable SPARK[1][2] subset of Ada, called Sparkel[3]. We will introduce the distinction between safety and liveness properties, and then focus primarily on techniques for the verification of safety properties, including the absence of race conditions and deadlocks. We will also discuss the issue of determinism vs. non-determinism in parallel and multi-threaded programs.
Formal methods research has made tremendous progress since the 1980s when a proof using a theorem prover was worthy of a Ph.D. thesis and a bug in a VLSI textbook was found using a model checker. Now, with advances in theorem proving, model checking, satisfiability modulo theories (SMT) solvers, and program analysis, the engines of formal methods are more sophisticated and are applicable and scalable: to a wide range of domains, from biology to mathematics; to a wide range of systems, from asynchronous systems to spreadsheets; and for a wide range of properties, from security to program termination. In this talk, I will present a few Microsoft Research stories of advances in formal methods and their application to Microsoft products and services. Formal methods use, however, is not routine?yet?in industrial practice. So, I will close with outstanding challenges and new directions for research in formal methods.
Systems are naturally constructed in hierarchies in which design choices made at higher levels of abstraction ``flow down'' to requirements on system components at lower levels of abstraction. Thus, whether an aspect of the system is a design choice or a requirement depends largely on one's vantage point within the hierarchy of system components. Furthermore, systems are often constructed middle-out rather than top-down; compatibility with existing systems and architectures, or availability of specific components influences high-level requirements. We believe that requirements and architectural design should be more closely aligned: that requirements models must account for hierarchical system construction, and that architectural design notations must better support specification of requirements for system components. In this presentation, I describe tools supporting iterative development of architecture and verification based on software models. We represent the hierarchical composition of the system in the Architecture Analysis & Design Language (AADL), and use an extension to the AADL language to describe requirements at different levels of abstraction for compositional verification. To describe and verify component-level behavior, we use Simulink and Stateflow and multiple analysis tools.
