Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 5 of 5
Full-Text Articles in Physical Sciences and Mathematics
Using Contracts To Guide The Search-Based Verification Of Concurrent Programs, Christopher M. Poskitt, Simon Poulding
Using Contracts To Guide The Search-Based Verification Of Concurrent Programs, Christopher M. Poskitt, Simon Poulding
Research Collection School Of Computing and Information Systems
Search-based techniques can be used to identify whether a concurrent program exhibits faults such as race conditions, deadlocks, and starvation: a fitness function is used to guide the search to a region of the program’s state space in which these concurrency faults are more likely occur. In this short paper, we propose that contracts specified by the developer as part of the program’s implementation could be used to provide additional guidance to the search. We sketch an example of how contracts might be used in this way, and outline our plans for investigating this verification approach.
Psyhcos: Parameter Synthesis For Hierarchical Concurrent Real-Time Systems, Étienne André, Yang Liu, Jun Sun, Jin Song Dong, Shang-Wei Lin
Psyhcos: Parameter Synthesis For Hierarchical Concurrent Real-Time Systems, Étienne André, Yang Liu, Jun Sun, Jin Song Dong, Shang-Wei Lin
Research Collection School Of Computing and Information Systems
Real-time systems are often hard to control, due to their complicated structures, quantitative time factors and even unknown delays. We present here PSyHCoS, a tool for analyzing parametric real-time systems specified using the hierarchical modeling language PSTCSP. PSyHCoS supports several algorithms for parameter synthesis and model checking, as well as state space reduction techniques. Its architecture favors reusability in terms of syntax, semantics, and algorithms. It comes with a friendly user interface that can be used to edit, simulate and verify PSTCSP models. Experiments show its efficiency and applicability
A Formal Semantics For Complete Uml State Machines With Communications, Shuang Liu, Yang Liu, Étienne André, Christine Choppy, Jun Sun, Bimlesh Wadhwa, Jin Song Dong
A Formal Semantics For Complete Uml State Machines With Communications, Shuang Liu, Yang Liu, Étienne André, Christine Choppy, Jun Sun, Bimlesh Wadhwa, Jin Song Dong
Research Collection School Of Computing and Information Systems
UML is a widely used notation, and formalizing its semantics is an important issue. Here, we concentrate on formalizing UML state machines, used to express the dynamic behaviour of software systems. We propose a formal operational semantics covering all features of the latest version (2.4.1) of UML state machines specification. We use labelled transition systems as the semantic model, so as to use automatic verification techniques like model checking. Furthermore, our proposed semantics includes synchronous and asynchronous communications between state machines. We implement our approach in USM2C, a model checker supporting editing, simulation and automatic verification of UML state machines. …
Verification Of Functional And Non-Functional Requirements Of Web Service Composition, Manman Chen, Tian Huat Tan, Jun Sun, Yang Liu, Jun Pang, Xiaohong Li
Verification Of Functional And Non-Functional Requirements Of Web Service Composition, Manman Chen, Tian Huat Tan, Jun Sun, Yang Liu, Jun Pang, Xiaohong Li
Research Collection School Of Computing and Information Systems
Web services have emerged as an important technology nowadays. There are two kinds of requirements that are crucial to web service composition, which are functional and non-functional requirements. Functional requirements focus on functionality of the composed service, e.g., given a booking service, an example of functional requirements is that a flight ticket with price higher than $2000 will never be purchased. Non-functional requirements are concerned with the quality of service (QoS), e.g., an example of the booking service’s non-functional requirements is that the service will respond to the user within 5 seconds. Non-functional requirements are important to web service composition, …
Improving Model Checking Stateful Timed Csp With Non-Zenoness Through Clock-Symmetry Reduction, Yuanjie Si, Jun Sun, Yang Liu, Ting Wang
Improving Model Checking Stateful Timed Csp With Non-Zenoness Through Clock-Symmetry Reduction, Yuanjie Si, Jun Sun, Yang Liu, Ting Wang
Research Collection School Of Computing and Information Systems
Real-time system verification must deal with a special notion of ‘fairness’, i.e., clocks must always be able to progress. A system run which prevents clocks from progressing unboundedly is known as Zeno. Zeno runs are infeasible in reality and thus must be pruned during system verification. Though zone abstraction is an effective technique for model checking real-time systems, it is known that zone graphs (e.g., those generated from Timed Automata models) are too abstract to directly infer time progress and hence non-Zenoness. As a result, model checking with non-Zenoness (i.e., existence of a non-Zeno counterexample) based on zone graphs only …