Cyber-Physical Systems (CPS) consist of software interacting with the physical world, such as robots, vehicles, and industrial processes. CPS are frequently responsible for the safety of lives, property, or the enviro...
详细信息
Cyber-Physical Systems (CPS) consist of software interacting with the physical world, such as robots, vehicles, and industrial processes. CPS are frequently responsible for the safety of lives, property, or the environment, and so software correctness must be determined with a high degree of certainty. To that end, simply testing a CPS is insufficient, as its interactions with the physical world may be difficult to predict, and unsafe conditions may not be immediately obvious. Formal verification can provide stronger safety guarantees but relies on the accuracy of the verified system in representing the real system. Bringing together verification and implementation can be challenging, as languages that are typically used to implement CPS are not easy to formally verify, and languages that lend themselves well to verification often abstract away low-level implementation details. Translation between verification and implementation languages is possible, but requires additional assurances in the translation process and increases software complexity;having both in a single language is desirable. This paper presents a formalization of MARVeLus, a CPS language which combines verification and implementation. We develop a metatheory for its synchronous refinement type system and demonstrate verified synchronous programs executing on real systems.
Robots and other cyber-physical systems are held to high standards of safety and reliability, and thus one must be confident in the correctness of their software. Formal verification can provide such confidence, but p...
详细信息
ISBN:
(纸本)9781450399074
Robots and other cyber-physical systems are held to high standards of safety and reliability, and thus one must be confident in the correctness of their software. Formal verification can provide such confidence, but programming languages that lend themselves well to verification often do not produce executable code, and languages that are executable do not typically have precise enough formal semantics. We present MARVeLus, a stream-based approach to combining verification and execution in a synchronous programming language that allows formal guarantees to be made about implementation-level source code. We then demonstrate the end-to-end process of developing a safe robotics application, from modeling and verification to implementation and execution.
During testing, an error in software can either propagate to the output variables or be masked before it reaches them. Error propagation and masking characteristics are crucial in software testing because they directl...
详细信息
During testing, an error in software can either propagate to the output variables or be masked before it reaches them. Error propagation and masking characteristics are crucial in software testing because they directly influence testing effectiveness. The testing community has hence focused on developing test mechanisms to promote the propagation and reduce masking of errors in software under test. However, little is known about how severely the errors propagate and are masked during software execution. Moreover, little is known about what influences software's propagation and masking characteristics. Thus, in this study, we performed experiments to investigate the behavior of errors during software execution. We chose six case examples and created mutants per case example by seeding an error into each one. We then executed the mutants with randomly selected test cases and investigated how many errors were propagated and masked. If an error was masked, we examined the cause. In addition, we investigated what percentage of errors in the mutants reached the output variables. This study provides insight into the characteristics of errors in terms of propagation and masking, which will help testers design test inputs and choose monitoring variables to properly handle the masking of errors during testing.
Our aim is to define the kernel of a simple and uniform programming model-the reactor model-which can serve as a foundation for building and evolving internet-scale programs. Such programs are characterized by collect...
详细信息
Our aim is to define the kernel of a simple and uniform programming model-the reactor model-which can serve as a foundation for building and evolving internet-scale programs. Such programs are characterized by collections of loosely-coupled distributed components that are assembled on the fly to produce a composite application. A reactor consists of two principal components: mutable state, in the form of a fixed collection of relations, and code, in the form of a fixed collection of rules in the style of Datalog. A reactor's code is executed in response to an external stimulus, which takes the form of an attempted update to the reactor's state. As in classical process calculi, the reactor model accommodates collections of distributed, concurrently executing processes. However, unlike classical process calculi, our observable behaviors are sequences of states, rather than sequences of messages. Similarly, the interface to a reactor is simply its state, rather than a collection of message channels, ports, or methods. One novel feature of our model is the ability to compose behaviors both synchronously and asynchronously. Also, our use of Datalog-style rules allows aspect-like composition of separately-specified functional concerns in a natural way. (C) 2008 Elsevier B.V. All rights reserved.
We investigate the benefits of using a synchronous data-flow language for programming critical real-time systems. These benefits concern ergonomy-since the dataflow approach meets traditional description tools used in...
详细信息
We investigate the benefits of using a synchronous data-flow language for programming critical real-time systems. These benefits concern ergonomy-since the dataflow approach meets traditional description tools used in this domain-and ability to support formal design and verification methods. We show, on a simple example, how the language LUSTRE, and its associated verification tool LESAR, can be used to design a program, to specify its critical properties, and to verify these properties. As the language LUSTRE and its uses have already been published in several papers (e.g., [11], [18]), we put particular emphasis on program verification. A preliminary version of this paper has been published in [28].
A key issue in the development of reliable embedded software is the proper handling of reactive control-flow, which typically involves concurrency. Java and its thread concept have only limited provisions for implemen...
详细信息
A key issue in the development of reliable embedded software is the proper handling of reactive control-flow, which typically involves concurrency. Java and its thread concept have only limited provisions for implementing deterministic concurrency. Thus, as has been observed in the past, it is challenging to develop concurrent Java programs without any deadlocks or race conditions. To alleviate this situation, the Light-weight synchronous Java (SJL) approach presented here adopts the key concepts that have been established in the world of synchronous programming for handling reactive control-flow. Thus SJL not only provides deterministic concurrency, but also different variants of deterministic preemption. Furthermore SJL allows concurrent threads to communicate with Esterel-style signals. As a case study for an embedded system usage, we also report on how the SJL concepts have been ported to the ARM-based Lego Mindstorms NXT system. We evaluated the SJL approach to be efficient and provide experimental results comparing it to Java threads.
We present ***, a synchronous reactive language that adds synchronous concurrency and preemption to JavaScript. Inspired from Esterel, *** simplifies the programming of non-trivial temporal behaviors as found in compl...
详细信息
ISBN:
(纸本)9781450376136
We present ***, a synchronous reactive language that adds synchronous concurrency and preemption to JavaScript. Inspired from Esterel, *** simplifies the programming of non-trivial temporal behaviors as found in complex web interfaces or IoT controllers and the cooperation between synchronous and asynchronous activities. *** is compiled into plain sequential JavaScript and executes on unmodified runtime environments. We use three examples to present and discuss ***: a simple web login form to introduce the language and show how it differs from JavaScript, and two real life examples, a medical prescription pillbox and an interactive music system that show why concurrency and preemption help programming such temporal applications.
Search strategies are crucial to efficiently solve constraint satisfaction problems. However, programming search strategies in the existing constraint solvers is a daunting task and constraint-based languages usually ...
详细信息
ISBN:
(纸本)9781450372497
Search strategies are crucial to efficiently solve constraint satisfaction problems. However, programming search strategies in the existing constraint solvers is a daunting task and constraint-based languages usually have compositionality issues. We propose space-time programming, a paradigm extending the synchronous language Esterel and timed concurrent constraint programming with backtracking, for creating and composing search strategies. In this formalism, the search strategies are composed in the same way as we compose concurrent processes. Our contributions include the design and behavioral semantics of spacetime programming, and the proofs that spacetime programs are deterministic, reactive and extensive functions. Moreover, spacetime programming provides a bridge between the theoretical foundations of constraint-based concurrency and the practical aspects of constraint solving. We developed a prototype of the compiler that produces search strategies with a small overhead compared to the hard-coded ones.
Using a new domain-theoretic characterisation we show that Berry's constructive semantics is a conservative approximation of the recently proposed sequentially constructive (SC) model of computation. We prove that...
详细信息
ISBN:
(纸本)9783642548338;9783642548321
Using a new domain-theoretic characterisation we show that Berry's constructive semantics is a conservative approximation of the recently proposed sequentially constructive (SC) model of computation. We prove that every Berry-constructive program is deterministic and deadlock-free under sequentially admissible scheduling. This gives, for the first time, a natural interpretation of Berry-constructiveness for shared-memory, multi-threaded programming in terms of synchronous cycle-based scheduling, where previous results were cast in terms of synchronous circuits. This opens the door to a direct mapping of Esterel's signal mechanism into boolean variables that can be set and reset under the programmer's control within a tick. We illustrate the practical usefulness of this mapping by discussing how signal reincarnation is handled efficiently by this transformation, which is of linear complexity in program size, in contrast to earlier techniques that had quadratic overhead.
This paper presents an embedding of polychronous programs into synchronous ones. Due to this embedding, it is not only possible to deepen the understanding of these different models of computation, but, more important...
详细信息
This paper presents an embedding of polychronous programs into synchronous ones. Due to this embedding, it is not only possible to deepen the understanding of these different models of computation, but, more importantly, it is possible to transfer compilation techniques that were developed for synchronous programs to polychronous programs. This transfer is nontrivial because the underlying paradigms differ more than their names suggest: Since synchronous systems react deterministically to given inputs in discrete steps, they are typically used to describe reactive systems with a totally ordered notion of time. In contrast, polychronous system models entail a partially ordered notion of time, and are most suited to interface a system with an asynchronous environment by specifying input/output constraints from which a deterministic controller may eventually be refined and synthesized. As particular examples for the mentioned cross fertilization, we show how a simulator and a verification backend for synchronous programs can be made available to polychronous specifications, which is a first step toward integrating heterogeneous models of computation.
暂无评论