Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 6 of 6
Full-Text Articles in Physical Sciences and Mathematics
Automatic Generation Of Provably Correct Embedded Systems, Shang-Wei Lin, Yang Liu, Pao-Ann Hsiung, Jun Sun, Jin Song Dong
Automatic Generation Of Provably Correct Embedded Systems, Shang-Wei Lin, Yang Liu, Pao-Ann Hsiung, Jun Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
With the demand for new and complicated features, embedded systems are becoming more and more difficult to design and verify. Even if the design of a system is verified, how to guarantee the consistency between the design and its implementation remains a big issue. As a solution, we propose a framework that can help a system designer to model his or her embedded system using a high-level modeling language, verify the design of the system, and automatically generate executable software codes whose behavior semantics are consistent with that of the high-level model. We use two case studies to demonstrate the …
An Analytical And Experimental Comparison Of Csp Extensions And Tools, Ling Shi, Yang Liu, Jun Sun, Jin Song Dong, Gustavo Carvalho
An Analytical And Experimental Comparison Of Csp Extensions And Tools, Ling Shi, Yang Liu, Jun Sun, Jin Song Dong, Gustavo Carvalho
Research Collection School Of Computing and Information Systems
Communicating Sequential Processes (CSP) has been widely applied to modeling and analyzing concurrent systems. There have been considerable efforts on enhancing CSP by taking data and other system aspects into account. For instance, CSP M combines CSP with a functional programming language whereas CSP# integrates high-level CSP-like process operators with low-level procedure code. Little work has been done to systematically compare these CSP extensions, which may have subtle and substantial differences. In this paper, we compare CSP M and CSP# not only on their syntax, but also operational semantics as well as their supporting tools such as FDR, ProB, and …
Verification Of Orchestration Systems Using Compositional Partial Order Reduction, Tian Huat Tan, Yang Liu, Jun Sun, Jin Song Dong
Verification Of Orchestration Systems Using Compositional Partial Order Reduction, Tian Huat Tan, Yang Liu, Jun Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
Orc is a computation orchestration language which is designed to specify computational services, such as distributed communication and data manipulation, in a concise and elegant way. Four concurrency primitives allow programmers to orchestrate site calls to achieve a goal, while managing timeouts, priorities, and failures. To guarantee the correctness of Orc model, effective verification support is desirable. Orc has a highly concurrent semantics which introduces the problem of state-explosion to search-based verification methods like model checking. In this paper, we present a new method, called Compositional Partial Order Reduction (CPOR), which aims to provide greater state-space reduction than classic partial …
Towards A Model Checker For Nesc And Wireless Sensor Networks, Manchun Zheng, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu
Towards A Model Checker For Nesc And Wireless Sensor Networks, Manchun Zheng, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu
Research Collection School Of Computing and Information Systems
Wireless sensor networks (WSNs) are expected to run unattendedly for critical tasks. To guarantee the correctness of WSNs is important, but highly nontrivial due to the distributed nature. In this work, we present an automatic approach to directly verify WSNs built with TinyOS applications implemented in the NesC language. To achieve this target, we firstly define a set of formal operational semantics for most of the NesC language structures for the first time. This allows us to capture the behaviors of sensors by labelled transition systems (LTSs), which are the underlying semantic models of NesC programs. Secondly, WSNs are modeled …
Verifying Stateful Timed Csp Using Implicit Clocks And Zone Abstraction, Jun Sun, Yang Liu, Jin Song Dong, Xian Zhang
Verifying Stateful Timed Csp Using Implicit Clocks And Zone Abstraction, Jun Sun, Yang Liu, Jin Song Dong, Xian Zhang
Research Collection School Of Computing and Information Systems
In this work, we study model checking of compositional real-time systems. A system is modeled using mutable data variables as well as a compositional timed process. Instead of explicitly manipulating clock variables, a number of compositional timed behavioral patterns are used to capture quantitative timing requirements, e.g. delay, timeout, deadline, timed interrupt, etc. A fully automated abstraction technique is developed to build an abstract finite state machine from the model. The idea is to dynamically create/delete clocks, and maintain/solve a constraint on the clocks. The abstract machine weakly bi-simulates the model and, therefore, LTL model checking or trace-refinement checking are …
Specifying And Verifying Event-Based Fairness Enhanced Systems, Jun Sun, Yang Liu, Jin Song Dong, Hai H. Wang
Specifying And Verifying Event-Based Fairness Enhanced Systems, Jun Sun, Yang Liu, Jin Song Dong, Hai H. Wang
Research Collection School Of Computing and Information Systems
Liveness/Fairness plays an important role in software specification, verification and development. Existing event-based compositional models are safety-centric. In this paper, we describe a framework for systematically specifying and verifying event-based systems under fairness assumptions. We introduce different event annotations to associate fairness constraints with individual events. Fairness annotated events can be used to embed liveness/fairness assumptions in event-based models flexibly and naturally. We show that state-of-the-art verification algorithms can be extended to verify models under fairness assumptions, with little computational overhead. We further improve the algorithm by other model checking techniques like partial order reduction. A toolset named Pat has …