ABSTRACT. Successful application of formal methods technologies to the development of a system is not just a matter of skillful use of formal methods tools and mathematical analysis techniques. It requires also establishing a constructive dialogue between formal methods experts and a multi-disciplinary team of engineers, domain experts, and end users of the system.

This dialogue is necessary to gain confidence that: - Formal models correctly capture the characteristics and functionalities of the system under development; - Formal properties correctly capture the intended meaning of requirements given in natural language; - Counter-examples produced in formal analysis results point out genuine design issues that need fixing, and not artifacts due to approximations used in the model.

The current generation of formal methods tools are not designed to facilitate this dialogue. They provide text-based front-ends, rich of mathematical details that non-experts of formal methods find hard to understand. These elements create communication barriers that can result in important delays in the development life-cycle, and overall reduced benefits from using formal methods.

This talk discusses a pragmatic approach to streamlining existing formal methods tools. The approach builds on the idea of extending formal methods tools with rapid prototyping capabilities. By this means, formal methods experts can create realistic prototypes that resemble the visual appearance of the system being developed. The behavior of the prototypes is driven by executable formal models. The prototypes can be used to produce interactive demos and scenario-based simulations suitable to discuss all aspects of the formal analysis effort, effectively eliminating the need to show the textual output produced by formal methods tools. Success stories based on the PVSio-web toolkit (www.pvsioweb.org) will be presented to illustrate the benefits of the approach. PVSio-web introduces prototyping capabilities in the PVS verification system. The toolkit has been used successfully over the past five years to support formal analysis of commercial devices and integration of formal methods in existing software development processes. It allowed effective communication of the formal analysis effort to a range of different stakeholders, including device developers, human factors specialists, regulatory agencies, procurement staff, and end users of the final system.

ABSTRACT. Industrial applications involving formal methods are still ex- ceptions to the general rule. Lack of understanding, employees without proper education, diculty to integrate existing development cycles, no explicit requirement from the market, etc. are explanations often heard for not being more formal. This article reports some experience about a game changer that is going to seamlessly integrate formal methods into safety critical systems engineering.

ABSTRACT. The guarded atomic action model of Event-B allows it to be applied to a range of systems including sequential, concurrent and distributed systems. However, the lack of explicit sequential structures in Event-B makes the task of sequential code generation difficult. Scheduled Event-B (SEB) is an extension of Event-B that augments models with control structures, supporting incremental introduction of control structures in refinement steps. SEB-CG is a tool for automatic code generation from SEB to executable code in a target language. The tool provides facilities for derivation of algorithmic structure of programs through refinement. The flexible and configurable design of the tool allows it to target various programming languages. The tool benefits from xText technology for a user-friendly text editor together with the proving facilities of Rodin platform for formal analysis of the algorithmic structure.

ABSTRACT. Building software packages from source is a complex and highly technical process. For this reason, most software comes with build instructions which have both a human-readable and an executable component. The latter in turn requires substantial infrastructure, which helps software authors deal with two major sources of complexity: first, generation and management of various build artefacts and their dependencies, and second, the differences between platforms, compiler toolchains and build environments.

This poses a significant problem for white-box analysis tools, which often require that the source code of the program under test is compiled into an intermediate format, like the LLVM IR. In this paper, we present divcc, a drop-in replacement for C and C++ compilation tools which transparently fits into existing build tools and software configuration management solutions. Additionally, divcc generates intermediate and native code in a single pass, ensuring that the final executable is built from the intermediate code that is being analysed.

ABSTRACT. In this paper, we report on our effort to design a fast, concurrent-safe hash table and implement it in C++, correctly. It is especially the latter that is the focus of this paper: concurrent data structures are notoriously hard to implement, and C++ is not known to be a particularly safe language. It however does offer unparalleled performance for the level of programming comfort it offers, especially in our area of interest -- parallel workloads with intense interaction.

For these reasons, we have enlisted the help of a software model checker (DIVINE) with the ability to directly check the C++ implementation. We discuss how such a heavyweight tool integrated into our engineering effort, what are the current limits of this approach and what kinds of assurances we obtained. Of course, we have applied the standard array of tools throughout the process -- unit testing, an interactive debugger, a memory error checker (valgrind) -- in addition to the model checker. This puts us in an excellent position to weigh them against each other and point out where they complement each other.

ABSTRACT. Despite the formal method community tends to overlook the problem, formal methods are sometimes difficult to use and not accessible to average users. On one hand, this is due to the intrinsic complexity of the methods and, therefore, some level of required expertise is unavoidable. On the other hand, however, the methods are sometimes hard to use because of lack of a user-friendly tool support. In this paper, we present our experience in addressing usability when developing a framework for the Abstract State Machines (ASMs) formal method. In particular, we discuss how we enhanced modeling, validation, and verification activities of an ASM-based development process. We also provide a critical review of which of our efforts have been more successful and those that, instead, have not obtained the results we were expecting. Finally, we outline other directions that we believe could further lower the adoption barrier of the method.

ABSTRACT. Reviews of various kinds are an established part of system development, but rely on the vigilance and thoroughness of the human participants for their quality. The use of formal methods as part of the toolkit deployed during review can increase those elements of dependability that formal methods do best to support. A methodology that proposes that formal techniques are used alongside conventional system construction practices during review is introduced. These can reduce the human burden of ensuring review quality, even if the coupling between the formal and conventional strands is not itself formally enforced. The approach advocated was inspired by experience of the use of formal methods in the INSPEX Project. This project targets the creation of a minaturised smart obstacle detection system, to be clipped onto a visually impaired or blind (VIB) person’s white cane, that would give aural feedback to the user about obstacles in front of them. The increasing complexity of such systems itself invites the use of formal techniques during development, but the hardware challenges preclude the application of textbook top-down formal methods. The use of formal methods in INSPEX is ad hoc, and the methodology proposed is an abstraction from the practical experience.