Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 4 of 4
Full-Text Articles in Physical Sciences and Mathematics
Model Checking Software Architecture Design, Jiexin Zhang, Yang Liu, Jing Sun, Jin Song Dong, Jun Sun
Model Checking Software Architecture Design, Jiexin Zhang, Yang Liu, Jing Sun, Jin Song Dong, Jun Sun
Research Collection School Of Computing and Information Systems
Software Architecture plays an essential role in the high level description of a system design. Despite its importance in the software engineering practice, the lack of formal description and verification support hinders the development of quality architectural models. In this paper, we present an automated approach to the modeling and verification of software architecture designs using the Process Analysis Toolkit (PAT). We present the formal syntax of the Wright# architecture description language together with its operational semantics in Labeled Transition System (LTS). A dedicated model checking module for Wright# is implemented in the PAT verification framework based on the proposed …
Translating Pddl Into Csp# - The Pat Approach, Yi Li, Jing Sun, Jin Song Dong, Yang Liu, Jun Sun
Translating Pddl Into Csp# - The Pat Approach, Yi Li, Jing Sun, Jin Song Dong, Yang Liu, Jun Sun
Research Collection School Of Computing and Information Systems
Model checking provides a way to automatically verify hardware and software systems, whereas the goal of planning is to produce a sequence of actions that leads from the initial state to the desired goal state. Recently research indicates that there is a strong connection between model checking and planning problem solving. In this paper, we investigate the feasibility of using a newly developed model checking framework, Process Analysis Toolkit (PAT), to serve as a planning solution provider for upper layer applications. We first carried out a number of experiments on different planning tools in order to compare their performance and …
A Formal Framework For Modeling And Validating Simulink Diagrams, Chunqing Chen, Jin Song Dong, Jun Sun
A Formal Framework For Modeling And Validating Simulink Diagrams, Chunqing Chen, Jin Song Dong, Jun Sun
Research Collection School Of Computing and Information Systems
Simulink has been widely used in industry to model and simulate embedded systems. With the increasing usage of embedded systems in real-time safety-critical situations, Simulink becomes deficient to analyze (timing) requirements with high-level assurance. In this article, we apply Timed Interval Calculus (TIC), a realtime specification language, to complement Simulink with TIC formal verification capability. We elaborately construct TIC library functions to model Simulink library blocks which are used to compose Simulink diagrams. Next, Simulink diagrams are automatically transformed into TIC models which preserve functional and timing aspects. Important requirements such as timing bounded liveness can be precisely specified in …
Machine-Assisted Proof Support For Validation Beyond Simulink, Chunqing Chen, Jin Song Dong, Jun Sun
Machine-Assisted Proof Support For Validation Beyond Simulink, Chunqing Chen, Jin Song Dong, Jun Sun
Research Collection School Of Computing and Information Systems
Simulink is popular in industry for modeling and simulating embedded systems. It is deficient to handle requirements of high-level assurance and timing analysis. Previously, we showed the idea of applying Timed Interval Calculus (TIC) to complement Simulink. In this paper, we develop machine-assisted proof support for Simulink models represented in TIC. The work is based on a generic theorem prover, Prototype Verification System (PVS). The TIC specifications of both Simulink models and requirements are transformed to PVS specifications automatically. Verification can be carried out at interval level with a high level of automation. Analysis of continuous and discrete behaviors is …