Time-Sensitive Networking (TSN) is a set of standards developed by the IEEE 802.1 working group to bring deterministic, low-latency, and reliable communication over standard Ethernet networks. Due to the plurality of mechanisms proposed by the standard, finding the best configuration for a given network topology is a complex and tedious task. In order to support the network designer, we have developed an environment to design, analyze, and optimize a network configuration. This environment also provides the capability to give formal guarantees on latencies, jitters and synchronization precision.

Aerospace systems are more and more distributed, both at equipment level, thanks to the emergence of multicore SoCs, and at system level, where architectures involve an ever-increasing number of nodes interconnected by digital networks. Computations distribution is a means to leverage the available processing power and achieve higher performances. It allows to reduce communication needs, by placing processing closer to actuators and sensors, and makes it possible to comply with various dependability and industrial objectives such as fault tolerance, industrial segregation of responsibilities, etc. This makes integration activities even more critical, due to the interaction complexity between the software components and their deployment on the hardware platform. Therefore, predictability, testability, and ultimately strong determinism are crucial high-level properties needed not only at equipment level but at the whole system scope, which cannot be tackled without changes in the design process. So, new programming and execution paradigms are required. This paper deals with a solution to support the distribution process, based on the sLET paradigm, which is applied to an aerospace landing system over a distributed system architecture.

The strategic implementation of Artificial Intelligence (AI) technologies in the industry requires extending conventional engineering disciplines to include AI-specific considerations. This allows the management and evaluation of risks associated with AI technologies, thereby unlocking their potential to improve system autonomy. Moreover, this allows to ensure a high level of confidence among stakeholders, such as regulatory authorities and clients. In this context, this paper provides an overview of the findings from the confiance.ai research program, which aims to develop methodological guidelines/ processes for engineering trustworthy AI systems. These processes are the result of collaborative efforts by a large group of experts focused on AI system trustworthiness. Data trustworthiness assessment and risk analysis are examples of these methodological processes.

Precision Timed (PRET) is a conceptual solution proposed in 2007 to address the ever increasing unpredictability of embedded processors, which results from features such as multi-level caches or deep pipelines. For many real-time systems, it is mandatory to compute a strict bound on the program's execution time. Yet, in general, computing a tight bound is extremely difficult. The rationale of PRET is to simplify both the programming language and the execution platform to allow precise execution times to be easily computed. ForeC is a PRET programming language. It is a multithreaded variant of C with a synchronous execution semantics. ForeC programs are designed to be executed on multi-core processors, built around either PRET cores or classical cores. A drawback of ForeC is that programs are single rate, i.e., all reactions must be implemented to run at the fastest rate imposed by the environment. This represents a high overhead, both at design time and at run-time. In this paper, we propose a multi-rate version of ForeC to improve its practicality and usability for industrial acceptance. We detail the syntax and semantics of the ForeC language in the context of multi-rate applications and present an implementation on a PRET multi-core architecture. Both the languages and its implementation are illustrated over a robotic application.

In this paper, we propose a new approach for the predictability and optimality of the inter-core communication and execution of tasks allocated on different cores of multicore architectures. Our approach is based on the execution of synchronous programs written in the ForeC programming language on deterministic architectures called PREcision Timed. The originality of the work resides in the time-triggered model of computation and communication that allows for a very precise control over the thread execution. Synchronization is done via configurable Time Division Multiple Access (TDMA) arbitrations where the optimal size and offset of the time slots are computed to reduce the inter-core synchronization costs. We implemented a robotic application and simulated it using MORSE, a robotic simulation environment. Results show that the model we propose guarantees time-predictable inter-core communication, the absence of concurrent accesses (without relying on hardware mechanisms), and allows for optimized execution throughput.

Abstract Event‐B is a formal notation and method for the systems development. The key feature of this method is to produce correct‐by‐construction system designs. Once the correct design is established, the remaining work is to generate or implement correct code from the design. Two main problems remain in the process from the correct‐by‐construction design to the correct software. First, the Event‐B design is “quasi‐correct” due to some technical limitations. For instance, it is still difficult to prove the liveness properties by the Rodin platform; it is not possible to construct the Event‐B design with floating‐point arithmetic, and sometimes, the Event‐B model is incomplete and must rely on the third‐party libraries. Therefore, a method is needed to complement these modeling and proof gaps. Secondly, proving the correctness of an automatic code generator is very difficult; therefore, a method is needed to guarantee the correctness of the produced code without proving the code generator. In this article, we address the above 2 problems by introducing an intermediate formal language called High‐Level Language (HLL) between the Event‐B models and the C code. The Event‐B model is translated to HLL with an additional schedule configuration, where Event‐B invariants and system invariants (here, deadlock‐freeness and liveness properties) are proved using a SAT‐based model checker called S3. This proof guarantees the correctness of the HLL model with respect to the Event‐B model. The C code is then automatically generated from the HLL model for most functions and is manually implemented for the third‐party ones according to the function contracts defined in Event‐B. The correctness of the generated C code is guaranteed using the equivalence proof, and the correctness of the implemented C code is guaranteed using the conformance proof. Through the article, we use a traffic light controller to illustrate the proposed method; then, we apply the method to an automatic protection function of a 3‐wheeled robot to evaluate its feasibility.

ISBN : 978-989-758-210-3

This paper presents a formal development process for safety-critical embedded Human-Machine Interface (HMI) systems. This formal approach is centered on the LIDL formal language and the S3 verification toolset. It is aimed at blurring the boundaries between modeling, design, verification and implementation for the development of HMI. From textual requirements to software, the development process integrates the following formal activities: modeling the behavioral aspect of user interfaces (UIs) using LIDL; translating LIDL to Lustre, with which we combine the functional library in Lustre; translating the Lustre design models into the HLL verification models; verifying formal properties expressed in HLL against the HLL model using the S3 toolset, and diagnosing design errors with the help of counterexample scenarios and debug tools. This formal development process is illustrated on a simple use case — part of the display component of an alert management system used in a three-wheeled robot.

This demo presents a virtual platform and its system design methodology for MPSoC ARM-Based FPGA applied on a use case. The focus is on the architectural exploration step and architecture implementation step. The platform is enabled by the SpaceStudio™tool suite, which incorporates novel research in virtual platform modeling, performance profiling, architectural exploration and system generation for MPSoC. The methodology is applied on the Image-Based Position Monitoring function of TwIRTee, a small three-wheeled rover. TwIRTee is the demonstrator of the INGEQUIP project conducted at the Institut de Recherche Technologique of Toulouse (IRT Saint- Exupéry).

For a long time, formal methods have been effectively applied to design and develop safety-critical systems to ensure safety and the correctness of desired functional behaviors through formal reasoning. The development of high confidence self-adaptive autonomous systems, such as Automatic Rover Protection(ARP), is one of the challenging problems in the area of verified software that needs formal reasoning and proof-based development. In this paper, we propose a methodology that reveals the issues involved in the formal modeling and verification of self-adaptive autonomous systems using correct by construction approach. This work also provides a set of guidelines for tacking the different issues to avoid collision by preserving the local and global properties of an autonomous system. We cater for the specification of functional requirements, timing requirements, spatial and temporal behavior, and safety properties. We present a refinement strategy, modeling patterns to capture the essence of a self-adaptive autonomous system, and a substantial example based approach on an industrial case study: TwIRTee. For developing the formal models of autonomous system, we use the Event-B modeling language and associated Rodin tools to check and verify the correctness of required system behavior and internal consistency under the given safety properties.

The development and validation of fault-tolerant computers for critical real-time applications are currently both costly and time consuming. Often, the underlying technology is out-of-date by the time the computers are ready for deployment. Obsolescence can become a chronic problem when the systems in which they are embedded have lifetimes of several decades. This paper gives an overview of the work carried out in a project that is tackling the issues of cost and rapid obsolescence by defining a generic fault-tolerant computer architecture based essentially on commercial off-the-shelf (COTS) components (both processor hardware boards and real-time operating systems). The architecture uses a limited number of specific, but generic, hardware and software components to implement an architecture that can be configured along three dimensions: redundant channels, redundant lanes, and integrity levels. The two dimensions of physical redundancy allow the definition of a wide variety of instances with different fault tolerance strategies. The integrity level dimension allows application components of different levels of criticality to coexist in the same instance. The paper describes the main concepts of the architecture, the supporting environments for development and validation, and the prototypes currently being implemented.