Synchronous embedded systems are becoming more and more complicated and are usually implemented with integrated hardware/software solutions. This implementation manner brings new challenges to the traditional model-driven design environments such as SCADE and STATEMATE, that supports pure hardware or software design. In this paper, we propose a co-design tool Tsmart-Edola to facilitate the system developers, and automatically generate the executable VHDL code and C code from the for- mal verified SyncBlock computation model. SyncBlock is a lightweight high-level system specification model with well defined syntax, simulation and formal semantics. Based on which, the graphical model editor, graphical simulator, verification translator, and code generator are implemented and seamlessly integrated into the Tsmart-Edola. For evaluation, we apply Tsmart-Edola to the design of a real-world train controller based on the international standard IEC 61375. Several critical ambiguousness or bugs in the standard are detected during formal verification of the constructed system model. Furthermore, the generated VHDL code and C code of Tsmart-Edola outperform that of the state-of-the-art tools in terms of synthesized gate array resource consumption and binary code size.

Today's distributed systems are commonly equipped with both synchronous and asynchronous components controlled with multiple clocks. The key challenges in designing such systems are (1) how to model multi-clocked local synchronous component, local asynchronous component, and asynchronous communication among components in a single framework. (2) how to ensure the correctness of model, and keep consistency between the model and the implementation of real system. In this paper, we propose a novel computation model named GalsBlock for the design of multi-clocked embedded system with both synchronous and asynchronous components. The computation model consists of several hierarchical compound and atom blocks communicating with data port connections. Each atom block can be refined as parallel mealy automata. The synchronous component can be captured in an atom block with the corresponding local control clock while the asynchronous component in an atom block without clock, and the asynchronous communications can be captured in the data port connections among blocks. The unified operational semantics and formal semantics are defined, which can be used for simulation and verification, respectively. Then, we can generate efficient VHDL code from the validated model, which can be synthesized into the FPGA processor for execution directly. We have developed the graphical modeling, simulation, verification, and code generation toolkit to support the computation model, and applied it in the design of a sub-system used in the real train communication control.

The key challenges of the model-driven approach to designing multi-clocked embedded systems are three-fold: (1) how to model local synchronous components and asynchronous communication between components in a single framework, (2) how to ensure the correctness of the model, and (3) how to maintain the consistency between the model and the implementation of the system. In this paper, we present Tsmart, a self-contained toolkit to address these three challenges. Tsmart seamlessly integrates (1) a graphical editor to facilitate the modeling of the complex behaviors and structures in an embedded system, (2) a simulator for interactive graphical simulation to understand and debug the system model, (3) a verication engine to verify the correctness of the system design, and (4) a synthesis engine to automatically generate ecient executable VHDL code from the model. The toolkit has been successfully applied to designing the main control system of a train communication controller, and the system has already been deployed and in operation. The evaluation of Tsmart on this real industrial application demonstrates the eectiveness and the potential of the toolkit.

Architecting real-time embedded systems is of the top significance during the design phase, especially in complex applications. Due to limited time and resource, to guarantee scheduling eminence without violating application-specific constraints is a challenging problem in architecture level. In this paper, we firstly present an enhanced transformation from AADL models to Cheddar input for schedulability analysis. With subprogram and delayed connection, this transformation is feasible for complex system designs. Based on schedulability analysis, we further propose a novel architecture selection engine, which evaluates scheduling performance through selection standards and application-specific constraints via satisfaction functions. With the proposed selection engine, information from both schedulability and real-time constraints are captured to pick up an optimal architecture. We apply the proposed approach on the architecture selection of an industrial control system in railway applications. Four candidate AADL architectures are transformed and analyzed for schedulability. Then in the selection engine, candidates are ranked within two application constraints. Compared to the selection of general criteria and traditional AHP, our engine excels at better schedulability and satisfaction on real-time application-specific constraints. Moreover, with adjustment on constraints, our engine shows delicate sensitivity by generating a modified selection. We believe the proposed approach can facilitate architecture design of real-time embedded systems.

In real-time embedded applications, interrupt-driven systems are widely adopted due to strict timing requirements. However, development of interrupt-driven systems is time-consuming and error-prone. To conveniently ensure a trustworthy system design and implementation is a challenging problem, especially in complex applications. In this paper, we present a novel domain-specific language called iDola to model interrupt-driven systems declaratively and concisely. A major strength of iDola is the feasibility to capture complex interrupt handling mechanism in real-time operating systems and target platforms, such as delayed service and buffered processing. We also propose the formal operational semantics and code generation algorithm of iDola, so that iDola models can be transformed to timed automata for verification and loaded to generate platform-specific codes. We apply iDola on the modeling of an industrial interrupt-driven system, multifunction vehicle bus controller which runs in an embedded environment with eCos operating system. Based on iDola, the system is modeled with a dispatcher which embodies advanced interrupt handling in eCos, including buffered interrupt service routine and deferred service routine. Through transformation, the system design is verified and design bugs are detected. Code generation is also executed using the proposed algorithm. Generated codes display comparatively equal performance in the real system. We believe iDola can facilitate building a trustworthy interrupt-driven system.

Programmable Logic Controllers (PLC) are widely used in industry. The reliability of the PLC is vital to many critical applications. This paper presents a novel approach to the symbolic analysis of PLC systems. The approach includes, (1) calculating the uncertainty characterization of the PLC system, (2) abstracting the PLC system as a Hidden Markov Model, (3) solving the Hidden Markov Model with domain knowledge, (4) combining the solved Hidden Markov Model and the uncertainty characterization to form a regular Markov model, and (5) utilizing probabilistic model checking to analyze properties of the Markov model. This framework provides automated analysis of both uncertainty calculations and performance measurements, without the need for expensive simulations. A case study of an industrial, automated PLC system demonstrates the effectiveness of our work.

Embedded systems are becoming increasingly popular due to their widespread applications and the reliability of them is a crucial issue. The complexity of the reliability analysis arises in handling the sequential feedback that make the system output depends not only on the present input but also the internal state. In this paper, we propose a novel probabilistic model, named sequential dependency model (SDM), for the reliability analysis of embedded systems with sequential feedback. It is constructed based on the structure of the system components and the signals among them. We prove that the SDM model is s Dynamic Bayesian Network (DBN) that captures: the spatial dependencies between system components in a single time slice, the temporal dependencies between system components of different time slices, and the temporal dependencies due to the sequential feedback. We initiate the conditional probability distribution (CPD) table of the SDM node with the failure probability of the corresponding system component. Then, the SDM model handles the spatial-temporal correlations at internal components as well as the higher order temporal correlations due to the sequential feedback with the computational mechanism of DBN, experiment results demonstrate the accuracy of our model.

The train control system is a safety-critical embedded system. In this system, all buses and devices share the real time communication protocol, which is described in the standard IEC 61375. Many systems that comply the standard have been implemented and used in the real world railway, however, their safety checking is highly nontrivial. In this paper, we focus on the formal verification and implementation of the protocol described in the standard. The protocol is modeled as a network of timed automata, which are synchronized to describe the procedure of connection establishment and data transmission among vehicles. The stochastic factors such as time delay and packet loss are modeled in the channel module. Afterwards, we abstract some safety critical properties that are important to guarantee the correctness of the protocol. These properties are verified with the model checker Uppaal. Two properties are violated in the verification, and two corresponding bugs in the standard are fixed and proposed to the IEC. In order to prove the bugs we find, we implement two versions of the standard. The first is for the original description of the standard, and the second is for our fixed description. Both versions are tested with the D113 (a widely used general Multifunction Vehicle Bus control system implemented by the Duagon company), and we find that the second version works well, while the first fails. The second version for the fixed protocol is now used in the real world subway.

Today’s system-on-chip and distributed systems are commonly equipped with multiple clocks. The key challenge in designing such systems is that heterogenous control-oriented and data-oriented behaviors within one clock domain, and asynchronous communications between two clock domains have to be captured and evaluated in a single framework. In this paper, we propose to use timed automata and synchronous dataflow to capture the dynamic behaviors of multi-clock embedded systems. A timed automata and synchronous dataflow based modeling and analyzing framework is constructed to evaluate and optimize the performance of multiclock embedded systems. Data-oriented behaviors are captured by synchronous dataflow, while synchronous control-oriented behaviors are captured by timed automata, and inter clock-domain asynchronous communication can be modeled in an interface timed automaton or a synchronous dataflow module with the CSP mechanism. The behaviors of synchronous dataflow are interpreted by some equivalent timed automata to maintain the semantic consistency of the mixed model. Then, various functional properties can be simulated and verified within the framework. We apply this framework in the design process of a sub-system that is used in real world subway communication control system

Programmable logic controller (PLC) system is a typical kind of embedded system that is widely used in industry. The complexity of reliability analysis of safety critical PLC systems arises in handling the temporal correlations among the system components caused by the run-time execution logic of the embedded ladder program. In this paper, we propose a novel probabilistic model for the reliability analysis of PLC systems, called run-time reliability model (RRM). It is constructed based on the structure and run-time execution of the embedded ladder program, automatically. Then, we present some custom-made conditional probability distribution (CPD) tables according to the execution semantics of the RRM nodes, and insert the reliability probability of each system component referenced by the node into the corresponding CPD table. The proposed model is accurate and fast compared to previous work as described in the experiment results.

Geometric algorithms are widely used in many scientific fields like computer vision, computer graphics. To guarantee the correctness of these algorithms, it's important to apply formal method to them. In this paper, we propose an approach to proving the correctness of geometric algorithms. The main contribution of the paper is that a set of proof decomposition rules is proposed which can help improve the automation of the proof of geometric algorithms. We choose TLA+2, a structural specification and proof language, as our experiment environment. The case study on a classical convex hull algorithm shows the usability of the method.

We present a pattern-based method to express time specifications in the language TLA+. A real-time module RealTimeNew is introduced to encapsulate the definitions of commonly used time patterns. We present a general framework to differentiate the temporal characterizations from system functionality with time constraints. The temporal specification is concise and provably as a refinement of its corresponding functional description without time. The method ameliorates the usability of TLA+in specifying and verifying time-sensitive systems. A case study is harnessed to illustrate and validate the approach.

In this paper, we developed a format for the specification of PLC systems using the specification language TLA+. Correctness properties for TLA+ specifications can be verified using the TLC model checker. The format we propose clearly distinguishes between user actions, system actions, and plant feedback. The different categories of actions are specified separately by TLA+ action formulas, which are then composed to form the overall specification. This separation makes us confident that we avoided overspecification, in particular of the environment. Working in a high-level language such as TLA+ allows a designer to focus on the essential features of a system specification. It also helps to avoid low-level encodings, which combined with parameterization leads to configurable and concise specifications. The resulting models can nevertheless be analyzed by the TLA+ model checker in a reasonable amount of time.