Synchronous language is routinely used to model safety-critical control systems. In recent years, it is gradually being applied to cyber-physical systems (CPS) which emphasise high levels of correctness and safety. It is based on the assumption that the system reacts instantaneously to input events and can compute the output before the next input event, so it is well suited for expressing temporal logic. However, it lacks effective constructs for expressing spatial properties in CPS. Moreover, spatio-temporal properties in CPS are indispensable, requiring not only qualitative analysis but also quantitative analysis. Therefore, we propose SELus, a new synchronous language based on Lustre, to provide the capability of modeling spatio-temporal properties in CPS, enabling the representation of spatial topological relationships and the performance of quantitative analysis on them. To formally verify the SELus model, we introduce a set of mapping rules to transform the SELus model into the Ptolemy II model. The resulting Ptolemy II model is used in Ptolemy II to perform quantitative analysis of the SELus model. Experiments are conducted on lane changing system, showcasing the usability and effectiveness of our language.

A Programmable Logic Controller (PLC) is an essentially domain-specific computer used to control physical equipment and is widely used in industrial control fields. It plays a crucial role in automating complex processes for industrial automation systems, requiring high reliability as code vulnerabilities can potentially lead to disasters. Therefore, vulnerability detection in PLC programs is of significant importance. However, the availability of tools supporting vulnerability detection in PLC programming languages is limited. This paper attempts to improve industrial security from the perspective of code security and proposes a static code analysis approach specifically designed for IEC 61131–3 Structured Text (ST) programs. This approach uses structural pattern matching and symbolic execution technology to identify program defects and improve quality by detecting problematic code structures and potential issues early in the development process, thereby reducing the debugging effort required during developments. Considering the characteristic of periodic loop execution in PLCs, we introduce the loop unwinding technique to collect constraints from subsequent execution cycles for detection purposes. Based on the aforementioned approach, we implement a static code analysis tool, ST-Checker and make a series of evaluations. The experimental results show that this method is feasible and can detect potential defects that existing PLC compilers cannot detect, improving the precision of defect detection with data dependencies.

Abstract In this paper, we consider the minimal unsatisfiable core (MUC) problem for linear temporal logic over finite traces (LTL$_{f}$), which nowadays is a popular formal-specification language for AI-related systems. Efficient algorithms to compute such MUCs can help locate the inconsistency rapidly in the written LTL$_{f}$ specification and are very useful for the system designers to amend the flawed requirement. As far as we know, there are no available tools off-the-shelf so far that provide MUC computation for LTL$_{f}$. We present here two generic approaches NaiveMUC and BinaryMUC to compute an MUC for LTL$_{f}$. Moreover, we introduce heuristics that are based on the Boolean unsatisfiable core (UC) technique to accelerate the two approaches, which are named NaiveMUC+UC and BinaryMUC+UC, respectively. In particular, for global LTL$_{f}$ formulas, we show that the MUC computation can be reduced to the pure Boolean MUC computation, which therefore conducts the GlobalMUC approach. Our experiments show that GlobalMUC performs the best to compute an MUC for global formulas, and BinaryMUC+UC is the best for an arbitrary unsatisfiable formula.

Programmable Logic Controllers (PLCs) are specialized computers extensively utilized in industrial control fields. Since they control industrial equipment, software faults in PLCs can result in significant losses. However, current testing for PLC programs is mainly manual, and there are very few automatic testing tools. Structured Text (ST) is one of the five PLC programming languages stipulated by the IEC 61131-3 standard, suitable for writing complex control logic. This paper proposes an automatic unit test case generation framework for ST programs based on Dynamic Symbolic Execution and PLC states, as well as a supporting algorithm, and implements the PLCAutoTester tool. PLCAutoTester supports the automatic generation of ST program unit test cases that comply with statement coverage, branch coverage, and MC/DC coverage criterion. We evaluated the PLCAutoTester using 20 PLC programs and compared it with S${}_{YM}$PLC. The experimental results show that PLCAutoTester can generate unit test cases with high coverage in a short time. And in 11 common programs, PLCAutoTester is able to generate test cases with almost the same statement coverage as S${}_{YM}$PLC while reducing the number of test cases by 95%.

The excellent model obtained through natural data training in deep learning is easily tampered with by adversarial examples. After discovering that, adversarial training has become the best way to defend against adversarial attacks and improve the robustness of the model. Since it is expensive to frequently calculate adversarial examples in each epoch during the training process, most people prefer to choose a single-step adversarial training method. However, the single-step adversarial training method will cause catastrophic overfitting and make the model lose robustness forever. In this paper, we explain adversarial training from the perspective of data augmentation, using artificial binary data to explore the reason for the occurrence of this overfitting. We propose two methods, VFSAT(Various fixed-stepsize single-step adversarial training) and GradSum, to prevent the overfitting in term of local smoothing and improve the robustness of the model obtained by single-step adversarial training. Simultaneously, experiments on CIFAR-10 and Tiny ImageNet datasets were constructed and the proof that single-step adversarial training could also resist multi-step adversarial attacks was derived.

SysML state machine (SysML-STM) is a modeling tool used in the Systems Modeling Language (SysML) to describe the behavior of a system. It is widely used in model-driven development (MDD). Formal methods are mathematical techniques to ensure the correctness, reliability and safety of software systems and hardware designs. In this paper, we introduce formal methods into MDD by transforming a SysML-STM model into a Uppaal timed automata. By formally verifying the system at an early stage of the development life-cycle, we aim to enhance the system's robustness. We design the mapping rules between the two models and have developed a tool, STMTU, to transform them directly. Our tool effectively leverage the benefits of formal verification techniques to ensure the correctness and reliability of the system. And the direct transformation of these models not only reduces the learning cost for developers but also helps to promote the wider adoption of formal methods.

As federated learning (FL) becomes more extensively employed, it attracts an increasing number of scholars and practitioners.In contrast to traditional decentralized machine learning approaches that acquire users' raw data, FL gathers locally updated gradients, protecting their privacy.However, different users may have disparate data distributions, resulting in underperformance of the federated model.It is beneficial to adapt the federated model to various data distributions.Numerous personalisation approaches have been examined, but most of them are limited to a single device with minimal data, making them susceptible to bias and overfitting.In fact, the data distributions of certain users are similar, and these similarities can be leveraged to increase the efficacy of personalisation.In this research, we describe a sparsity-based clustering method, as well as a federated personalisation strategy based on it.Our method mitigates the impact of non-IID data and generates more accurate local models.The trials reveal that it outperforms several of its counterparts.

Summary Model checking and static analysis have been well studied for program verification. Because of the ability to describe the stack, the pushdown system (PDS) has become a perfect model that is able to accurately model procedure calls and mimic the program's stack. Thus, it is not only a good model for sequential programs but for malware detection as well. However, with the increase of the complexity of programs, the size of models becomes huge as well. Thus, the model‐checking problem is expensive to solve. The computational tree logic (CTL) is a widely used logic and its model checking problem of PDSs can be reduced to the emptiness analysis of an alternating Büchi pushdown system (ABPDS) by determining whether there is an accepting run. When the size of a PDS is huge, the computations can be time‐consuming. To overcome this limitation, we propose a parallel solution. We propose a parallel framework based on the Compute Unified Device Architecture and the corresponding parallel algorithms to solve the emptiness problem of ABPDSs. Moreover, in order to effectively utilize the graphics processing unit, we design a new data structure of variables and an algorithm of management of thread scheduling for the parallel model. We implement our algorithms in a tool and compare our tool to a CTL model checker for PDS as a benchmark. The comparison results indicate an encouraging performance speedup.

Programmable logic controllers (PLC), which are widely applied in modern industrial control systems (ICS), work as the controller of sensors and actuators in ICS. These systems require strict correctness, especially for safety-critical systems. Currently, increasingly ICS move to “come online” scenarios to enhance cyber-physical features, but it makes them more vulnerable due to acquiring increased interconnection accompanied by weakening physical isolation. Moreover, with the more complex controlling environment, such as hundreds of more I/O points and more diverse field buses, the incorrect executions of PLC might cause the failure of the overall ICS. In this article, we examine how the security and safety of running PLC could be enhanced in both developing and deploying stages of ICS. We propose a novel application of runtime verification to guarantee the security and safety of real-world ICS. As a variant of temporal logic, PLC past linear temporal logic (PPLTL) is proposed to specify the security and safety properties of PLC. Using PPLTL, we synthesize monitors to improve the PLC program’s security and safety as a partner of testing and static verification. Our monitors provide twofold processing in a nonintrusive manner: One is filtering abnormal input data before invading the original programs, the other is double-checking the output signals before driving the actuators. We use several case studies and benchmarks to demonstrate the efficiency of the approach. The empirical results show that the time overhead and memory occupation are tiny.

Programmable logic controllers (PLCs) are broadly used in the safety-critical industrial field, which requires high reliability to avoid catastrophes. Data flow testing (DFT) focuses on data flow relationships in a program and has a stronger fault-detection ability than other control flow-based testing. However, there is no automated testing tool supporting DFT for PLC programs. Hence, we propose an automated data flow testing framework for PLC programs. Our DFT framework is based on dynamic symbolic execution (DSE). Considering the cyclic execution feature of PLC programs, our approach needs reachable states which can be provided by branch testing. Besides, our approach improves testing performance through a novel guided path search algorithm. Furthermore, we evaluate our approach on several programs to demonstrate that this approach is practical and effective.

There are quite tight timing requirements in deterministic low latency network. The IEEE 802.1 Time-Sensitive Networking (TSN) task group has proposed several traffic shapers to satisfy real-time communications requirements. Traditionally, the performance of TSN is analyzed by simulations, whereas these methods cannot cover all corner cases. This paper firstly presented formal models of the TSN’s time-aware and peristaltic shapers using UPPAAL, tactically solving the problem mentioned above. Afterward, we verified some properties of the shapers models, of which the results could evaluate whether these shapers are able to satisfy strict timing requirements or not. Based on the models, we can discuss about the performance of time-critical traffic combining the preemption mechanism. More-over, we can also analyze resource utilization and transmission latency. Under the time properties analysis and verification of TSN traffic shapers, we can provide engineers with an accessible reference that may assist them in developing the TSN.

Since programmable logic controllers (PLCs) control safety-critical infrastructures, examining the PLC software satisfies the high-reliability specifications necessary to ensure the safeness of PLCs.However, prior works have limitations in finding defects in the PLC source code.Static verification techniques suffer from notable false positives without capturing runtime behavior.The symbolic execution and conformance testing technique captures the relations of inputs and outputs.It is not sufficient to consider only the data constraints as the PLC operates in real-time.In this paper, we propose a novel approach in the detection of the runtime behavior of PLC programs with incorporated time constraints.This testing approach automatically finds implementation errors in PLC programs by mining invariants from runtime traces.As the existing tools mine only data or time invariants which are inadequate to test PLC programs, our approach focuses on the interplay of data and time invariants.Dynamically detected datatime invariants are then checked with the safety specifications.We evaluate the usefulness of our approach in a real-life case.The experimental results show that the proposed approach can find errors in PLC programs effectively.

With the development of artificial intelligence, machine learning algorithms are currently being used in more and more fields, such as autonomous driving, medical diagnosis, etc. In recent years, much research focuses on property verification of machine learning models. As one of the machine learning models, the tree ensemble model's structure is amicable to formal verification, but large models still prove hard to verify due to the combinatorial path explosion. This paper presents a violation-driven, sound but incomplete method from a testing perspective. We generate an explanation model of the original model and verify it formally. After a narrowed search space is obtained, we verify the original model by a testing-based method. A counterexample is then proof that the original model violates the property. We elaborate our method through a case study in detail. And we have developed our method into a tool called TEPV (Tree Ensemble Property Verification) and tested it on datasets of various sizes. The experiment demonstrates that our approach is scalable and works well on large tree ensemble models.

Simulink has been widely used in model-based design and development. While we witness a growing demand on testing and verification for safety-critical systems, it remains a challenge to verify Simulink models, due largely to a lack of standardized formal semantics for Simulink. In this paper, we propose a comprehensive framework that allows us to automatically verify Simulink models. Our proposed framework is equipped with Signal Temporal Logic (STL) for system requirements specification and employs a formal method to translate Simulink models into UPPAAL timed automata, which can then be verified automatically by UPPAAL (against their STL specification). A novelty of our work is the integration of Simulink models with STL, allowing us to express and then verify complex time properties that may be found difficult by existing work. In our translation of Simulink models, we adopt symbolic execution to reduce the size of the translated automata that can produce accurate results. We also demonstrate the feasibility and effectiveness of the proposed framework via a case study of an autonomous driving system.

With the development of the industrial control system, programmable logic controllers (PLCs) are increasingly adopted in the process automation. Moreover, many PLCs play key roles in safety-critical systems, such as nuclear power plants, where robust and reliable control programs are required. To ensure the quality of programs, testing and verification methods are necessary. In this article, we present a novel methodology which applies model checking to verifying PLC programs. Specifically, we focus on the structured text (ST) language which is a widely used, high-level programming language defined in the electro-technical commission (IEC) 61131-3 standard. A formal model named behavior model (BM) is defined to specify the behavior of ST programs. An algorithm based on variable state analysis for automatically extracting the BM from an ST program is given. An algorithm based on the automata-theoretic approach is proposed to verify linear temporal logic properties on the BM. Finally, a real-life case study is presented.

The fault tree (FT) is a well-established and well-understood technique for reliability assessment and fault analysis in the aerospace field. Recently, some researches combine FTs with other technologies to optimize the fault analysis process, but there are still some issues. One issue is that some ignored logical contradictions generate unreachable subtrees in the process of building FTs. Another is that when performing fault diagnosis, some studies only focus on the basic events or treat the basic events and intermediate events equally, which results in some special situations not being considered. To tackle the above two issues, we propose a new methodology for simplifying the FT and then performing fault diagnosis. By transforming the FT into a state transition diagram (STD), we perform satisfiability analysis on unreachable subtrees to simplify the FT. Then when performing fault diagnosis, we use the transformed STD to handle basic events and intermediate events separately. This can reduce unnecessary operations and identify multiple failure combinations. Finally, we use a case to demonstrate the effectiveness of our proposed methodology.

Abstract The functions of automobiles are becoming increasingly intelligent, which leads to the increasing number of electrical control units for one automobile. Hence, it makes software migration and extension more complicated. In order to avoid these problems, the standard OSEK/VDX has been proposed jointly by a German automotive company consortium and the University of Karlsruhe. This standard provides specifications for the development of automotive software, this standard has become one of the major standards for real-time automotive operating systems (OSs). Since errors in the automotive OS may pose threat to the safety of people in a vehicle, it is necessary to verify the correctness of the OSEK OS which is used by many manufacturers around the world. Formal methods can be adopted to verify the correctness of both software and hardware. Therefore, we propose a formal model of the OSEK OS at the code level and verify three significant properties of the OSEK-based system. In this study, the code-level OSEK OS is verified to ensure compliance with the specifications. An automotive OS always requires that the systemreacts in a timelymanner to external events and performs the computations within the timing constraints. However, there is a possibility that the running time of the tasks exceeds the timing requirements due to the complexity of the tasks. Therefore, by referring to one of the extensions of the OSEK OS, Automotive Open System Architecture (AUTOSAR), we proposed tpOSEK, which is capable of extending the OSEK OS with a timing protection mechanism in AUTOSAR in this study. In our previous study, it was verified that the higher-priority task cannot be preempted by lower-priority tasks. In this paper, after improvement made to the OSEK OS model by adding interrupt service routine models and alarms, and extension of the OSEK OS model with a timing protection model, we have verified that tpOSEK satisfies three significant properties, which include deadlock f ree, complete and no timeout. These properties represent the basic conditions for the systemto run smoothly. If such properties as deadlock f ree and complete are satisfied, it means no deadlock is encountered by this system and all of the tasks can be scheduled completely. Moreover, if the property timeout cannot be satisfied, it means that none of the tasks would miss the deadline. Based on the tpOSEK model, the correct timing protection APIs can be designed at the code level. Thus, by extending the OSEKOSwith theseAPIs,we can update theOSEKOS faster and the need tomodify the dependent applications can be removed. Furthermore, we have constructed formal models for two industrial cases based on tpOSEK OS to demonstrate the soundness of our methods.

Industrial networks are the cornerstone of modern industrial control systems. Performing security checks of industrial communication processes helps detect unknown risks and vulnerabilities. Fuzz testing is a widely used method for performing security checks that takes advantage of automation. However, there is a big challenge to carry out security checks on industrial network due to the increasing variety and complexity of industrial communication protocols. In this case, existing approaches usually take a long time to model the protocol for generating test cases, which is labor-intensive and time-consuming. This becomes even worse when the target protocol is stateful. To help in addressing this problem, we employed a deep learning model to learn the structures of protocol frames and deal with the temporal features of stateful protocols. We propose a fuzzing framework named SeqFuzzer which automatically learns the protocol frame structures from communication traffic and generates fake but plausible messages as test cases. For proving the usability of our approach, we applied SeqFuzzer to widely-used Ethernet for Control Automation Technology (EtherCAT) devices and successfully detected several security vulnerabilities.

A programmable logic controller (PLC) is essentially a computer dedicated to industrial control which is widely used in the field of global automation control. However, PLC software bugs can result in economic losses and even personal safety issues. PLC software must be thoroughly tested regarding function, structure, safety, and other aspects to avoid accidents. Existing PLC tools are mainly based on the manual setting of input data, which is not only unable to be well automated but also cannot provide information about code coverage. This paper presents an automated test case generation approach for a Structured Text (ST) language to reduce the cost of testing, using dynamic symbolic execution. We apply this method to implement the coverage-based automated test case generation tool STAutoTester. We have evaluated STAutoTester on 21 programs. The experimental results show that STAutoTester can effectively handle these programs. For 11 ST programs, STAutoTester reduces, on average, 87.5% of generated test cases compared to SYMPLC.

In this paper, we attempt to improve industrial safety from the perspective of communication security. We leverage the protocol fuzzing technology to reveal errors and vulnerabilities inside implementations of industrial network protocols(INPs). Traditionally, to effectively conduct protocol fuzzing, the test data has to be generated under the guidance of protocol grammar, which is built either by interpreting the protocol specifications or reverse engineering from network traces. In this study, we propose an automated test case generation method, in which the protocol grammar is learned by deep learning. Generative adversarial network(GAN) is employed to train a generative model over real-world protocol messages to enable us to learn the protocol grammar. Then we can use the trained generative model to produce fake but plausible messages, which are promising test cases. Based on this approach, we present an automatical and intelligent fuzzing framework(GANFuzz) for testing implementations of INPs. Compared to prior work, GANFuzz offers a new way for this problem. Moreover, GANFuzz does not rely on protocol specification, so that it can be applied to both public and proprietary protocols, which outperforms many previous frameworks. We use GANFuzz to test several simulators of the Modbus-TCP protocol and find some errors and vulnerabilities.

With the development of "Industry 4.0", the scale and complexity of industrial control system grow rapidly. Hence, the analysis and verification of such systems face really big challenges. Industry requires a reliable approach for decomposing the existing complex system model to multiple fine-grained and interactive models. In this paper, we propose a general event-triggered language named IMCL for modeling industrial control systems. IMCL can describe the physical resources and system in one unified model. Following the given physical resource constraints, we present the reliable and efficient decomposition and collaboration algorithms based on IMCL models to meet the industrial requirements. In particular, we have implemented these algorithms in a tool and get same encouraging results.

As an integral part of the Ethernet standard IEEE 802.3, the Ethernet Powerlink protocol is widely used in the automation industry. It is a software-based solution and achieves some real-time capabilities. It satisfies data transmission demands by guaranteeing communication with very high speed and accuracy. In effort to make implementing Powerlink protocol easier, we build a formal Powerlink model via Communicating Sequential Processes (CSP) and implement it in the model checker Process Analysis Toolkit (PAT). Based on the model, we simulate Managing Node (MN) and Controlled Node (CN) behaviors in a Powerlink cycle. We verify and evaluate the scheduling algorithm given in the official tutorial, and present an improved algorithm. At last, we verify some properties including deadlock about the Powerlink protocol and whether it exhibits problematic behavior when it is operating.

Model checking suffers from the infamous state space explosion problem. In this paper, we propose an approach, named GPURC, to utilize the Graphics Processing Units (GPUs) to speed up the reachability verification. The key idea is to achieve a dynamic load balancing so that the many cores in GPUs are fully utilized during the state space exploration. To this end, we firstly construct a compact data encoding of the input transition systems to reduce the memory cost and fit the calculation in GPUs. To support a large number of concurrent components, we propose a multi-integer encoding with conflict-release accessing approach. We then develop a BFS-based state space generation algorithm in GPUs, which makes full use of the GPU memory hierarchy and the latest dynamic parallelism feature in CUDA to achieve a high parallelism. GPURC also supports a parallel collaborative event synchronization approach and integrates a GPU hashing method to reduce the cost of data accessing. The experiments show that GPURC can give significant performance speedup (average 50X and up to 100X) compared with the traditional sequential algorithms.

In vehicular ad-hoc network, Media AccessControl (MAC) is one of the technologies which determinewhether the information is transferred reliably and timely or not. It is also a key to the quality of service of self organizationnetworks. Some behaviors of the MAC protocol can be estimatedby experiment and simulation. But the main drawback of thesemethods is that the estimation can not be accurate to support theenough confidence. In this paper, we complete the preciseanalysis of the MAC protocol by probabilistic model checking. First, based on the nature of MAC, its dynamic behavior isabstracted into a probabilistic timed automata which candescribe non-deterministic, continuous time and the probabilityselection of MAC. Then we calculate the probability of the datasent successfully and the probability of the backoff counterreaching the maximum value. The analysis result shows that theprobability of conflict in 802.11p is much smaller than the 802.11standard. Therefore the waiting time in 802.11p is significantlyreduced and in the case of fast-moving, the data can be senttimely. Further we calculate the maximum expect conflictnumber under the different values of maximum backoff and thelongest time to complete the data transmission. The result showsthat when the value of maximum backoff increases, the numberof collisions that occurred in 802.11p tends to be stable, which isless than the 802.11 standard's collisions, and the average speedof the data transmission in 802.11p is as four times faster as the802.11 standard.

In the design of dependable software for real-time and embedded systems, the quantitative analysis of program behavior and system performance is a crucial but extremely difficult issue, the challenge of which is exacerbated due to the random city and nondeterminism of interrupt events and the corresponding handling behaviors. Moreover, time analysis is also need to be taken into account for such kinds of systems. Thus the research on a theory which integrates interrupt behaviors and time analysis seems to be important and challenging. In this paper, we propose an interrupt modeling language pIML including the probabilistic feature to describe the programs with interrupts. We explore a probabilistic operational semantics to depict the actions of pIML. Meanwhile, we also implement this operational semantics we proposed on Maude platform, which fill the gap between the theory and practice. Maude supports rewriting logic, equational logic, and etc. The rewrite rules of rewriting logic can very well implement the transition rules of probabilistic operational semantics. Based on this implementation, it is very convenient to simulate the program written in pIML and analyze the behaviors of program in the presence of interrupts quantitatively.

As one of the most practical protocols, Time-Triggered CAN protocol (TTCAN), which is time triggered to ensure the real-time capability required by embedded systems, has been widely used in the automotive electric system development. In this paper, we present a formal model of the TTCAN protocol using Timed Communicating Sequential Processes (Timed CSP). All the components in the protocol are abstracted as CSP processes, thus the basic transmission in TTCAN is converted into the communication between different CSP processes. Besides, an error handling model is also proposed to capture the exception in the protocol. Finally, we use model checker Process Analysis Toolkit (PAT) to verify whether we can achieve model caters for some properties, which are specified using Linear Temporal Logic (LTL) formulas. Based on the verification results, our TTCAN model turns out to match the specification.

The AUTOSAR (AUTomotive Open System ARchitecture) is an open standard in automotive industry, aiming at unifying the methodology of the automotive software development. It is drawing increasing attention because of its great concern about the safety of automotive electronics. The safety of automotive electronics greatly depends on the Operating System (OS) components, which fully implement the functionality part of automotive applications. However, taking the complex timing protection mechanism of AUTOSAR OS and random occurrences of interrupt requests (IRs) into consideration, it is hard for the developers to design and configure the OS components correctly or even reconcilably. In this paper, we focus on the timing properties and propose an automatic verification framework, in which developers could analyze the timing behaviors and devise the OS components configuration. Furthermore, three important timing properties are expressed and can be verified in our framework, namely, schedulability, non-fault-propagation, and consistency. As a reduced version of AUTOSAR OS and auxiliary analysis modules have been implemented based on Real-Time Maude, developers could easily employ the tool to experiment with different configurations of OS components.

For hybrid systems, hybrid automata based tools are capable of verification while Matlab Simulink/Stateflow is proficient in simulation. In this paper, a methodology is developed in which the formal verification tool PHAVer and simulation tool Matlab are integrated to analyze and verify hybrid systems. For application of this methodology, a Platform Screen Doors System (abbreviated as PSDS), a subsystem of the subway, is modeled with formal verification techniques based on hybrid automata and Matlab Simulink/Stateflow charts, respectively. The models of PSDS are simulated by Matlab and verified by PHAVer. It is verified that the sandwich situation can be avoided under time interval conditions. We conclude that this integration methodology is competent in verifying Platform Screen Doors System.

Interrupt mechanism is indispensable in embedded software due to lots of factors such as switching context and enhancing efficiency. In this context, the traditional way to ensure the correctness of software will not remain in force. Having the interrupt is envolved, the complicated and nondeterminism environment should be taken into consideration during the verification process. In this paper, we propose a novel way to verify the interrupt safety properties based on low-level binary code. At first, an Abstract xBIL is transformed from the xBIL with the time and interrupt properties reserved. xBIL [1] is a binary intermediate language we proposed to represent the machine instructions on multiple architectures. Afterwards, we present an automatic way to construct the Discrete-Time Markov Chains [2] from the Abstract xBIL code. After that, the properties can be easily generated and quantitative analysis could be performed. To prove the feasibility of our approach, we have applied our method to the verification of a commercial automotive operating system and it is proved to be of great help with the development of software.

As an automotive industry standard of operating system specification, OSEK/VDX is widely applied in the process of designing and implementing the static operating system and the corresponding interfaces for automotive electronics. It is challenging to explore an effective method to support large-scale correctness verification of OSEK/VDX specification. In this paper, we employ process algebra CSP to describe and reason about a real code-level OSEK/VDX operating system. Thus the whole system is formally modeled as a CSP process which is encoded and implemented in process analysis toolkit (PAT). Furthermore, the expected properties are described and expressed in terms of the first-order logic. The properties are also established and verified in our framework. The result indicates that the whole system is deadlock-free and the scheduling scheme is sound with respect to the specification.

OSEK/VDX Operating System Specification is a standard in automotive industry with a long history. Dozens of mature industrial operating systems are based on this specification and widely applied in the products of major automotive manufacturers. The verification of the operating system products is always a hard nut to crack. In this paper, we propose a formal specification of OSEK/VDX Operating System based on Hoare Logic, which helps us to get rid of the confusion and ambiguities of the informal specification. In this framework, the formalization of all the Application Programming Interfaces are made. As a case study, we link our framework to the formal verification tool VCC. Some errors are detected in a market-upcoming operating system product based on our framework. We conclude that our framework is feasible in verification of operating system.

This paper presents an approach to validation and verification of the WSCDL specification. In order to validate whether the CDL document is well defined or not, we introduce OCL to precisely describe the constraints which was expressed by natural language, and design a simple validator to check the static properties of the CDL document. The validator is created based on a Java model and the Java model is generated according to the UML diagrams with OCL constraints which is used to describe CDL specification. To verify the dynamic properties of CDL document, we model the behavior of CDL document with Java, so that Java Pathfinder model checker can be applied to check the desired properties. The assert activity is introduced to the CDL specification for describing the logic properties, to facilitate the verification process. A case study is given and it shows that our approach is both effective and practical. Moreover, this approach can check almost every kinds of CDL document, even the documents including exception block or finalize block.