Software Modeling Techniques and the Semantic Web (2009)
Web [1] as the next generation of web in which data are given well-defined and machine-understandable semantics so that they can be processed by intelligent software agents. Semantic Web can be...
Machine-Assisted Proof Support for Validation Beyond Simulink (2009)
Chunqing Chen, Jin Song Dong, Jun Sun
Abstract. 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...
Formal Specification-based Online Monitoring (2009)
Hui Liang, Jing Sun, Jin Song Dong, Roger Duke, Rudolph E. Seviora
With current trends towards more complex software system and use of higher level languages, a monitoring technique is of increasing importance for the areas such as performance enhancement,...
Semantic Web Languages – Towards an Institutional Perspective ∗ (2008)
Abstract. The Semantic Web (SW) is viewed as the next generation of the Web that enables intelligent software agents to process and aggregate data autonomously. Ontology languages provide basic...
Relating �-calculus to Object-Z (2008)
Kenji Taguchi, Jin Song Dong, Gabriel Ciobanu
Software systems have become increasingly distributed, dynamic and mobile. The complex state and dynamic interfaces of software components and their concurrent interactions provide challenging...
Generic fault tolerant software architecture reasoning and customization (2008)
Ling Yuan, Jin Song Dong, Jing Sun, Hamid Abdul Basit
Abstract—This paper proposes a novel heterogeneous software
Mechanical Verification of Fault Tolerant Architecture in a Prototype Verification System (2008)
Ling Yuan, Jin Song Dong, Jing Sun
Abstract. In this paper, we present an approach to embed our formal Generic Fault Tolerant Software Architecture (GFTSA) model in the PVS theorem prover to achieve automatic verification support for...
Modeling and Customization of Fault Tolerant Architecture using Object-Z/XVCL (2008)
This paper proposes a novel heterogeneous software architecture FTA (Fault Tolerant Architecture). FTA incorporates idealized fault tolerant component concept and coordinated error recovery mechanism...
Chunqing Chen, Jin Song Dong, Jun Sun
(TIC) is a highly expressive set-based notation for specifying and reasoning about embedded real-time systems. However, it lacks mechanical proving support, as its verification usually involves...
A Tools Environment for Developing and Reasoning about Ontologies (2008)
Jin Song Dong, Yuzhang Feng, Yuan Fang Li, Jun Sun
Started in the beginning of 2001, the Semantic Web is regarded by many as the next generation of the Web. Ontology languages are the building blocks of Semantic Web as they provide basic vocabularies...
Ling Yuan, Jin Song Dong, Jing Sun, Hamid Abdul Basit
Abstract — This paper proposes a novel heterogeneous software
RDF FRAMEWORK INSTITUTIONS (2008)
Dorel Lucanu, Yuan Fang Li, Jin Song Dong
The Semantic Web is a vision of enabling software agents to autonomously understand, process and integrate Web resources. This ability is based on semantically marking up Web resources using...
Chapter XIII Linking UML with Integrated Formal Techniques (2008)
Jing Liu, Jin Song Dong, Kun Shi, Brendan Mahony
The challenge for complex systems specification is how to visually and precisely capture static, dynamic and real-time system properties in a highly structured way. In particular, requirement...
Reasoning About Timed CSP Models (2008)
Jin Song Dong, Xian Zhang, Jun Sun, Ping Hao
Abstract. HORAE is an interactive system which supports composing and reasoning of Timed CSP process descriptions. Timed CSP extends CSP by introducing the capability to quantify temporal aspects of...
ABSTRACT TCOZ Approach to Semantic Web Services Design (2008)
Complex Semantic Web (SW) services may have intricate data state, autonomous process behavior and concurrent interactions. The design of such SW service systems requires precise and powerful...
Design synthesis from interaction and state-based specifications (2008)
Abstract—Interaction-based and state-based modeling are two complementary approaches of behavior modeling. The former focuses on global interactions between system components. The latter...
Semantic Space: An Infrastructure for (2008)
Smart Spaces, Xiaohang Wang, Jin Song Dong, Chungyau Chin, Ravipriya Hettiarachchi, Daqing Zhang
Semantic Space is a pervasive computing infrastructure that exploits Semantic Web technologies to support explicit representation, expressive querying, and flexible reasoning of contexts in smart...
Web Ontology Verification and Analysis in the Z Framework * (2008)
Dorel Lucanuyuan, Fang Li, Jin Song Dong, Yuan Fang Li, Jin Song Dong
Dorel Lucanu Faculty of Computer Science "A.I.Cuza " University
Sensor Network Design: Introducing Active Sensor Process (2008)
Jin Song Dong, Jun Sun, Xian Zhang, Jing Sun
Abstract. Wireless sensor network has shown a wide range of promising applications as well as challenges. In recent years, sensors have been equipped with significant processing, memory, and...
Relating π-calculus to Object-Z (2008)
Kenji Taguchi, Jin Song Dong, Gabriel Ciobanu
Software systems have become increasingly distributed, dynamic and mobile. The complex state and dynamic interfaces of software components and their concurrent interactions provide challenging...
Software Modeling Techniques and the Semantic Web (2008)
bination of RACER, Z/EVES [12] and the Alloy Analyser [10] tools. An illustration on how DAML can be used to build a Semantic Web environment for supporting, extending and integrating various...
The Semantics of Extended SOFL (2008)
Recently SOFL (Structured-Object-based-Formal Language) has been extended to a formal object-oriented language and method while keeping its structured features. This extension allows powerful...
A XML/XSL Approach to Visualize and Animate TCOZ (2008)
Jing Sun, Jin Song Dong, Jing Liu, Hai Wang
The challenge for system speci cation is how to visually and precisely capture static, dynamic and real-time system properties in a highly structured way. Timed Communicating Object-Z (TCOZ) is an...
A Reasoning Tool for Timed CSP based on Constraint Solving (2008)
Timed CSP extends CSP by introducing a capability to quantify temporal aspects of sequencing and synchronization. It is a powerful language to model real-time reactive systems. However, there is no...
Generating MSCs from an Integrated Formal (2008)
Specification Language Jin, Jin Song Dong, Shengchao Qin, Jun Sun
The requirements capture of complex systems requires powerful mechanisms for specifying system state, structure and interactive behaviors. Integrated formal specification languages are well suited...
Capturing Concurrent Interactions of Mission Computer Tasks (2008)
Safety critical systems, such as aviation systems controlled by software, often have hard real-time requirements. Producing the correct result at the right time is the fundamental goal of such...
Verifying OWL and ORL Ontologies in PVS (2008)
Jin Song Dong, Yuzhang Feng, Yuan Fang Li
The Semantic Web vision is being realized to reach the full potential of the Web. Semantic data modeling is the foundation of the Semantic Web. The Web Ontology Language (OWL) and OWL Rules Language...
An Object-Oriented Approach tothe Formal Speci cation of ODP Trader (2007)
An Object-Z formal speci cation of the ODP Trader is presented which concisely captures the hierarchical context structure, the distribution of information and the communication aspects of the...
Mark Utting, Ian Toyn, Jing Sun, Andrew Martin, Jin Song Dong, David Currie
Abstract. This paper proposes an XML format for standard Z. We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new...
Semantic Space: A Semantic Web-Based Infrastructure for Smart Spaces (2007)
Xiaohang Wang, Daqing Zhang, Jin Song Dong, Chunyau Chin
Semantic Space is a pervasive computing infrastructure that exploits the use of Semantic Web technologies to support explicit representation, expressive querying and flexible reasoning of contexts in...
A Combined Approach to Checking Web Ontologies ABSTRACT (2007)
The understanding of Semantic Web documents is built upon ontologies that define concepts and relationships of data. Hence, the correctness of ontologies is vital. Ontology reasoners such as RACER...
ABSTRACT TCOZ Approach to Semantic Web Services Design (2007)
Complex Semantic Web (SW) services may have intricate data state, autonomous process behavior and concurrent interactions. The design of such SW service systems requires precise and powerful...
Liveness plays an important role in system requirements. Fairness conditions are an effective way of expressing liveness properties. Previous studies on liveness and fairness have been state-based,...
From Live Sequence Charts to Distributed Implementation (2007)
Mechanized generation of prototypes from high-level specifications has long been an ultimate challenge for software engineering. One high-level specification of great interest is scenario-based...
An Integral Formal Approach to Semantic Work Environments Design (2007)
Wang, Hai H., Dong, Jin Song, Sun, Jing, Payne, Terry R., Gibbins, Nicholas, Li, Yuan-Fang, ...
An Integral Formal Approach to Semantic Work Environments Design (2007)
Wang, Hai H., Dong, Jin Song, Sun, Jing, Payne, Terry R., Gibbins, Nicholas, Li, Yuan-Fang, ...
Semantic Web Languages – Towards an Institutional Perspective (2006)
Lucanu, Dorel, Li, Yuan Fang, Dong, Jin Song
Abstract. The Semantic Web (SW) is viewed as the next generation of the Web that enables intelligent software agents to process and aggregate data autonomously. Ontology languages provide basic...
Semantic Web Languages – Towards an Institutional Perspective (2006)
Lucanu, Dorel, Li, Yuan Fang, Dong, Jin Song
Abstract. The Semantic Web (SW) is viewed as the next generation of the Web that enables intelligent software agents to process and aggregate data autonomously. Ontology languages provide basic...
A Reasoning Method for Timed CSP based on Constraint Solving (2006)
Jin Song Dong, Ping Hao, Jun Sun, Xian Zhang
Abstract. Timed CSP extends CSP by introducing a capability to quantify temporal aspects of sequencing and synchronization. It is a powerful language to model real time reactive systems. However,...
Verification of Computation Orchestration via Timed Automata (2006)
Jin Song Dong, Yang Liu, Jun Sun, Xian Zhang
Abstract. Recently, a promising programming model called Orc has been proposed to support a structured way of orchestrating distributed web services. Orc is intuitive because it offers concise...
From Live Sequence Charts to Distributed Implementations (2005)
Jin Song Dong, Jun Sun, Jaffar Joxan, Jun Sun, Jin Song Dong
tutorial article, which has been submitted for publication in a journal or for consideration by the commissioning organization. The report represents the ideas of its author, and should not be taken...
A Formal Approach to Semantic Web Services Design (2004)
Jin Song DONG, Yuanfang LI, Hai WANG
Complex Semantic Web (SW) services may have intricate data state, autonomous process behavior and concurrent interactions. The design of such SW service systems requires precise and powerful...
A Combined Approach to Checking Web Ontologies (2004)
Dong, Jin Song, Lee, Chew Hung, Lee, Hian Beng, Li, Yuan Fang, Wang, Hai
The understanding of Semantic Web documents is built upon ontologies that define concepts and relationships of data. Hence, the correctness of ontologies is vital. Ontology reasoners such as RACER...
Verifying OWL and ORL Ontologies in PVS (2004)
Dong, Jin Song, Feng, Yuzchang, Li, Yuan-Fang
The Semantic Web vision is being realized to reach the full potential of the Web. Semantic data modeling is the foundation of the Semantic Web. The Web Ontology Language (OWL) and OWL Rules Language...
Verifying OWL and ORL Ontologies in PVS (2004)
Dong, Jin Song, Feng, Yuzchang, Li, Yuan-Fang
The Semantic Web vision is being realized to reach the full potential of the Web. Semantic data modeling is the foundation of the Semantic Web. The Web Ontology Language (OWL) and OWL Rules Language...
A formal approach to semantic web services design (2004)
Jin Song Dong, Yuanfang Li, Hai Wang, Jaffar Joxan
tutorial article, which has been submitted for publication in a journal or for consideration by the commissioning organization. The report represents the ideas of its author, and should not be taken...
Relating π-calculus to Object-Z (2004)
Kenji Taguchi, Jin Song Dong, Gabriel Ciobanu
Software systems have become increasingly distributed, dynamic and mobile. The complex state and dynamic interfaces of software components and their concurrent interactions provide challenging...
Timed Patterns: TCOZ to Timed Automata (2004)
Jin Song Dong, Ping Hao, Sheng Chao Qin, Jun Sun, Wang Yi
The integrated logic-based modeling language, Timed Communicating Object Z (TCOZ), is well suited for presenting complete and coherent requirement models for complex real-time systems. However, the...
Jin Song DONG, Ping HAO, Sheng Chao QIN, Jun SUN, Yi WANG
The integrated logic-based modeling language, Timed Communicating Object Z (TCOZ), is well suited for presenting more complete and coherent requirement models for complex real-time systems. However,...
Checking and Reasoning about Semantic Web through Alloy (2003)
Jin Song Dong, Jing Sun, Hai Wang
Abstract. Semantic Web (SW), commonly regarded as the next generation of the Web, is an emerging vision of the new Web from the Knowledge Representation and the Web communities. The Formal Methods...
D.: ZML: XML Support for Standard Z (2003)
Mark Utting, Ian Toyn, Jing Sun, Andrew Martin, Jin Song Dong, Nicholas Daley, ...
Abstract. This paper proposes an XML format for standard Z.We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new...
A Semantic Foundation for TCOZ in Unifying Theories of Programming Shengchao Qin (2003)
Shengchao Qin, Jin Song Dong, Wei-ngan Chin
Unifying Theories of Programming(UTP) can provide a formal semantic foundation not only for programming languages but also for more expressive specification languages. We believe UTP is particularly...
Checking and Reasoning about Semantic Web (2003)
Through Alloy Jin, Jin Song Dong, Jing Sun, Hai Wang
Semantic Web (SW), commonly regarded as the next generation of the Web, is an emerging vision of the new Web from the Knowledge Representation and the Web communities. The Formal Methods community...
Reasoning about Semantic Web in Isabelle/HOL (2003)
Yue Tang School, Yue Tang, Jin Song Dong
Semantic Web is regarded as the next generation of the World Wide Web. It provides not only the structure of the web but also meaningful semantics for the information presented. To make Semantic Web...
D.: ZML: XML Support for Standard Z (2003)
Nicholas Daley, Nicholas Daley, Mark Utting, Mark Utting, Mark Utting, Ian Toyn, ...
Abstract. This paper proposes an XML format for standard Z. We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new...
ZML:XML support for standard Z. (2002)
Utting, Mark, Toyn, Ian, Sun, Jing, Martin, Andrew, Dong, Jin Song, Daley, Nicholas, ...
This paper proposes an XML format for standard Z. We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new proposal is...
ZML:XML support for standard Z. (2002)
Utting, Mark, Toyn, Ian, Sun, Jing, Martin, Andrew, Dong, Jin Song, Daley, Nicholas, ...
This paper proposes an XML format for standard Z. We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new proposal is...
Jin Song Dong, Jing Sun, Hai Wang
The World Wide Web provides an important infrastructure for a promising environment for formal specification and design activities because it allows sharing of various design models and provides...
XML-based Static Type Checking and Dynamic Visualization for TCOZ (2002)
Jin Song Dong, Yuan Fang Li, Jing Sun, Jun Sun, Hai Wang
TCOZ
XML-based Static Type Checking and Dynamic Visualization for TCOZ (2002)
Jin Song Dong, Yuan Fang Li, Jing Sun, Jun Sun, Hai Wang
Abstract. Timed Communicating Object Z(TCOZ) combinesObject-Z’s strengths in modelling complex data and state with TCSP’s strengths in modeling real-time concurrency. Based on our previous work...
Z Approach to Semantic Web (2002)
Jin Song Dong, Jing Sun, Hai Wang
Abstract. The Semantic Web (SW)service is a web application using Semantic Web techniques which usually involve cooperation between several intelligent agents. The design of SW systems requires...
An Overview of Mobile Object-Z (2002)
Abstract. Mobile Object-Z (MobiOZ) is an extended notation of Object-Z with mobile and communication primitives required for mobile agent applications. In this paper, we will give an overview of the...
XML-Based Static Type Checking and Dynamic Visualization for TCOZ (2002)
Jin Song Dong, Yuan Fang Li, Jing Sun, Jun Sun, Hai Wang
Timed Communicating Object Z(TCOZ) combinesObject-Z's strengths in modelling complex data and state with TCSP's strengths in modeling real-time concurrency. Based on our previous work on...
Semantic Web for Extending and Linking Formalisms Jin Song Dong, Jing Sun,an Ha Wa8 (2002)
School Ofceooz Bh, Jin Song Dong, Jing Sun, Hai Wang
The diversity of various formal specification techniques and the need for their e#ective combinations requires an extensible and integrated supporting environment. The Webprovides infrastructure for...
Z Approach toSD5R666 Web Jin Song Dong, Jing Sun,an Ha (2002)
School Of Computing, Jin Song Dong, Jing Sun, Hai Wang
TheSemaAflz Web (SW)service isa weba)L1z54)V1 using Sema) tic Web techniques whichusua)K involvecoopera1K] between severa intelligent antell The design of SW systems requires precise modelling...
Deep Semantic Links of TCSP and Object-Z: TCOZ Approach (2002)
Formal methods can be used in e#ective combination only if the semantic links between individual methods are clearly established. This paper discusses the semantic design of TCOZ, a language blended...
event, time and diagram in system modelling (2001)
The design of complex systems requires powerful mechanisms for modeling state, concurrent events, and real-time behavior; as well as for visualising and structuring systems in order to control...
event, time and diagram in system modelling (2001)
The design of complex systems requires powerful mechanisms for modeling state, concurrent events, and real-time behavior; as well as for visualising and structuring systems in order to control...
event, time and diagram in system modelling (2001)
The design of complex systems requires powerful mechanisms for modeling state, concurrent events, and real-time behavior; as well as for visualising and structuring systems in order to control...
Timed Communicating Object Z (2000)
This paper describes a timed, multithreaded object modeling notation for specifying real-time, concurrent, and reactive systems. The notation Timed Communicating Object Z (TCOZ) builds on...
Timed Communicating Object Z (2000)
Brendan Mahony And, Brendan Mahony, Jin Song Dong
This paper describes an integration of Object Z and Timed CSP, called Timed Communicating Object Z (TCOZ), and presents a case study on using TCOZ to specify a realtime multilift system. TCOZ builds...
Timed Communicating Object Z (2000)
This paper describes a timed, multithreaded object modeling notation for specifying real-time, concurrent, and reactive systems. The notation Timed Communicating Object Z (TCOZ) builds on...
An Object Semantic Model of SOFL (1999)
SOFL (Structured-Object-based-Formal Language) is recently proposed to combine the advantagesof formal methods, structured methods and object-oriented methodology into one method for software...
An Object Semantic Model of SOFL (1999)
SOFL (Structured-Object-based-Formal Language) is recently proposed to combine the advantagesof formal methods, structured methods and object-oriented methodology into one method for software...
An Object Semantic Model of SOFL (1999)
SOFL (Structured-Object-based-Formal Language) is recently proposed to combine the advantagesof formal methods, structured methods and object-oriented methodology into one method for software...
Sensors and Actuators in TCOZ (1999)
Brendan Mahony Jin, Jin Song Dong
Timed Communicating Object Z (TCOZ) combines Object-Z's strengths in modeling complex data and algorithms with Timed CSP's strengths in modeling real-time concurrency. TCOZ inherits...
Active objects have their own thread of control and passive objects are controlled by others. In Object-Z, all objects are modelled as passive objects. Timed Communicating Object Z (TCOZ) extends the...
Network Topology and a Case Study in TCOZ (1998)
Object-Z is strong in modeling the data and operations of complex systems. However, it is weak in specifying real-time and concurrent systems. The Timed Communicating Object-Z (TCOZ) extends Object-Z...
Blending Object-Z and Timed CSP: An introduction to TCOZ (1997)
Brendan Mahony Jin, Jin Song Dong
Object-Z is an extension to the Z language designed to facilitate specification in an object-oriented style. It is an excellent tool for modeling data and algorithms, but its object semantics are...
Formal Engineering of Software Library Systems (1997)
Steven Ross Atkinson, Steven Ross Atkinson, Jin Song Dong, Alena Griffiths, Andrew Hussey, Ian Maccoll, ...
The reuse of complete software developments and the processes used to create them has the potential to significantly ease the process of software engineering, by providing a source of verified...
Using Object-Z to Specify Object-Oriented Programming Languages (1996)
Jin Song Dong, Roger Duke, Jin Song, Dong Roger Duke
In this paper, we present a case study for using formal object-oriented specification languages, such as Object-Z, to specify the semantics of objectoriented programming languages. The key idea in...
Formal object modelling techniques and denotational semantics studies / (1995)
Includes bibliography.
Formal object modelling techniques and denotational semantics studies (1995)
Includes bibliography.
Living with Free Type and Class Union (1995)
There are two constructs in the formal specification language Object-Z for modelling polymorphic and recursive structures. One construct, the free type, is adopted from the Z specification language....
An Object-Oriented Approach to the Formal Specification of ODP Trader (1993)
this paper, Object-Z is used to give an object-oriented specification which concisely captures the hierarchical context structure, the distribution of information and the communication aspects of the...
An Object-Oriented Approach to the Formal Specification of ODP Trader (1993)
this paper, Object-Z is used to give an object-oriented specification which concisely captures the hierarchical context structure, the distribution of information and the communication aspects of the...
Overview of the Semantics of TCOZ
Object-Z is an extension to the Z language designed to facilitate specification in an object-oriented style. It is an excellent tool for modelling data and operations, but its object semantics are...