Search

Determinism is a key concern in the certification of software for safety-critical systems. In this paper, we evaluate the role of determinism in certification standards, using airborne software as example. We analyze and speculate how the requirements and underlying concepts related to determinism can be adapted for Machine Learning algorithms.In addition, we systematically identify and analyze a large set of factors that contribute to variations of behavior in machine learning systems across multiple levels. Our suggestion is that such variability factors are handled in a similar fashion to failure modes in current software and systems development.We propose that the method followed and the identified set of factors is taken as a step towards a global catalog that can assist both developers and assessors in attaining certifiable machine learning systems.

This paper describes a tool-supported method for the formal verification of Ada programs. It presents ATOS, a tool that automati- cally extracts a model in SPIN from an Ada Program, together with a set of properties that state the correctness of the model. ATOS is also capable of extracting properties from user-provided annotations in Ada programs, inspired by the Spark Annotation language. The goal of ATOS is to help in the verification of sequential and concurrent Ada pro- grams based on model checking. The paper introduces the details of the proposed mechanisms, as well as the results of experimental validation, through a case study., Fundação para a Ciência e a Tecnologia (FCT)

This chapter describes the formal TLA + models of the OpenComRTOS Layer 1 Interaction Entities (L1-Entities). The L1-Entities represent the API (Application Programmer’s Interface) of OpenComRTOS used by the Task entities to build up the application. There are also so-called Layer 0 entities but these are not accessible to the user. The L1 Entities are also all derived from a common so-called Hub Entity. As we will see later, the L1-Entities represent services the operating system offers to the user. The L1-Entities names represent the type of service they provide.

Model checking (Clarke et al. 1999; Holzmann 2003b; Lamport 2002a) is a flexible and powerful technique for verifying systems formally with automated tools. In principle, it makes this task easy for the user: given a formal system description and certain conditions to be satisfied, the automated checker either confirms that the system satisfies the conditions, or provides a counterexample.

This paper introduces a rigorous methodology for requirements specification of systems that react to external stimulus by evolving through different operational modes. In each mode different functionalities are provided. Starting from a classical state-machine specification, the envisaged methodology interprets each state as a different mode of operation endowed with an algebraic specification of the corresponding functionality. Specifications are given in an expressive variant of hybrid logic which is, at a later stage, translated into first-order logic to bring into scene suitable tool support. The paper’s main contribution is to pro- vide rigorous foundations for the method, framing specification logics as institutions and the translation process as a comorphism between them., Fundação para a Ciência e a Tecnologia (FCT)

In this chapter, we discuss the requirements and specifications for the OpenComRTOS project from the point of view of its capabilities to support applications in meeting real-time requirements. As this is related to a distributed real-time operating system this is rather unique as most RTOS are designed for single processor systems and if not, they assume a shared memory architecture whereby the address space is global. OpenComRTOS on the other hand makes no such assumptions, but assumes that a processor has local memory and that the hardware allows to communicate somehow between the processors’ memory. It is a network model, but allowing to emulate it by shared memory if this is available. Hence the term “network-centric” RTOS. In this context, we also explain the CSP background that is still present in the conceptual design of OpenComRTOS.

OpenComRTOS is part of a systematic, formalised systems and software engineering methodology for embedded systems with a supporting environment and tools. While OpenComRTOS can be used independently of it, users will benefit from using the methodology in an integrated way. This methodology is characterised by two key concepts: unified semantics and interacting entities. When used in combination, they result in a better control of the engineering process leading to the development of systems and products. OpenComRTOS plays an important role in this approach as it is the system software layer allowing the mapping of the abstract interacting entities at the modeling level into concrete concurrent instances.

Tasks in OpenComRTOS interact using an intermediate Hub entity. This way the interaction is decoupled from the tasks themselves. Different temporal semantics (waiting, non-waiting, and waiting with timeout) of tasks synchronization are formalised. Conclusions are drawn on correct usage confirming the correctness of the original CSP semantics.

The previous chapters of this book concentrated the theoretical foundations of OpenComRTOS and the formal modelling effort that was done in order to develop a trustworthy Real Time Operating System (RTOS). This chapter concentrates on the development of applications which utilise OpenComRTOS, as provided by OpenComRTOS-Suite 1.3. It is designed as a tutorial the reader can follow step by step. Section 9.1 gives a detailed introduction to OpenVE (the main development tool of the OpenComRTOS-Suite) to develop a Semaphore-loop executing on a single win32-node. The resulting project is then extended in Sect. 9.2 to utilise multiple nodes (MP), by introducing a second win32-node and connecting the two win32-nodes using TCP/IP. This illustrates how easy it is to construct distributed systems using the OpenComRTOS-Suite.

We briefly show that the resulting architecture generates very small code (5 KB for the distributed version) resulting in better performance and better safety properties.

As mentioned in Chap. 4, mathematics is the main intellectual tool for the genuine systems designer. In particular, the user of automated model or proof checkers can benefit from mathematical reasoning about both the system descriptions (e.g. programs) and the conditions (e.g. invariants, temporal formulas) in various respects.

This chapter discusses the implementation architecture of OpenComRTOS. This is done by using a small test program, called theSemaphore Loop. It follows a top down approach by first explaining the Semaphore Loop itself, including a definition of the Semaphore in terms of OpenComRTOS. This is followed by an explanation of what happens when a Task sends a request to the OpenComRTOS Kernel, taking as example the signalling and testing of a Semaphore. This example then is extended to a system consisting of two processing nodes, connected via a link, each of which executing part of the Semaphore Loop example. While the logical behaviour is the same, the resulting changes in the execution are discussed.