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
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 …
Specifying And Verifying Sensor Networks: An Experiment Of Formal Methods, Jin Song Dong, Jing Sun, Jun Sun, Kenji Taguchi, Xian Zhang
Specifying And Verifying Sensor Networks: An Experiment Of Formal Methods, Jin Song Dong, Jing Sun, Jun Sun, Kenji Taguchi, Xian Zhang
Research Collection School Of Computing and Information Systems
With the development of sensor technology and electronic miniaturization, wireless sensor networks have shown a wide range of promising applications as well as challenges. Early stage sensor network analysis is critical, which allows us to reveal design errors before sensor deployment. Due to their distinguishable features, system specification and verification of sensor networks are highly non-trivial tasks. On the other hand, numerous formal theories and analysis tools have been developed in formal methods community, which may offer a systematic method for formal analysis of sensor networks. This paper presents our attempt on applying formal methods to sensor network specification/verification. An …
Timed Automata Patterns, Jin Song Dong, Ping Hao, Shengchao Qin, Jun Sun, Wang Yi
Timed Automata Patterns, Jin Song Dong, Ping Hao, Shengchao Qin, Jun Sun, Wang Yi
Research Collection School Of Computing and Information Systems
Timed Automata have proven to be useful for specification and verification of real-time systems. System design using Timed Automata relies on explicit manipulation of clock variables. A number of automated analyzers for Timed Automata have been developed. However, Timed Automata lack composable patterns for high-level system design. Specification languages like Timed Communicating Sequential Process (CSP) and Timed Communicating Object-Z (TCOZ) are well suited for presenting compositional models of complex real-time systems. In this work, we define a set of composable Timed Automata patterns based on hierarchical constructs in time-enriched process algebras. The patterns facilitate the hierarchical design of complex systems …
A Scalable Approach To Multi-Style Architectural Modeling And Verification, Stephen Wong, Jing Sun, Ian Warren, Jun Sun
A Scalable Approach To Multi-Style Architectural Modeling And Verification, Stephen Wong, Jing Sun, Ian Warren, Jun Sun
Research Collection School Of Computing and Information Systems
Software Architecture represents the high level description of a system in terms of components, external properties and communication. Despite its importance in the software engineering process, the lack of formal description and verification support limits the value of developing architectural models. Automated formal engineering methods can provide an effective means to precisely describe and rigorously verify intended structures and behaviors of software systems. In this paper, we present an approach to support the design and verification of software architectural models using the Alloy analyzer. Based on our earlier work, we propose a fundamental library for specifying system structures in terms …
A Formal Model Of Semantic Web Service Ontology (Wsmo) Execution, Hai H. Wang, Nick Gibbins, Terry R. Payne, Ahmed Saleh, Jun Sun
A Formal Model Of Semantic Web Service Ontology (Wsmo) Execution, Hai H. Wang, Nick Gibbins, Terry R. Payne, Ahmed Saleh, Jun Sun
Research Collection School Of Computing and Information Systems
Semantic Web services have been one of the most significant research areas within the semantic Web vision, and have been recognized as a promising technology that exhibits huge commercial potential. Current semantic Web service research focuses on defining models and languages for the semantic markup of all relevant aspects of services, which are accessible through a Web service interface. The Web service modelling ontology (WSMO) is one of the most significant semantic Web service framework proposed to date. To support the standardization and tool support of WSMO, a formal semantics of the language is highly desirable. As there are a …