Huibiao Zhu

J. Syst. Archit., 2022

Translating CPS with Shared-Variable Concurrency in SpaceEx.

[BibT_eX]

[DOI]

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2022

Modeling and Verifying AUPS Using CSP.

[BibT_eX]

[DOI]

Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering, 2022

Formal Verification of COCO Database Framework Using CSP.

[BibT_eX]

[DOI]

Peimu Li

Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering, 2022

MEA: A Framework for Model Checking of Mutual Exclusion Algorithms Focusing on Atomicity.

[BibT_eX]

[DOI]

Junfu Luo

Proceedings of the Parallel and Distributed Computing, Applications and Technologies, 2022

Formalization and Verification of SIP Using CSP.

[BibT_eX]

[DOI]

Proceedings of the Parallel and Distributed Computing, Applications and Technologies, 2022

Denotational and Algebraic Semantics for the CaIT Calculus.

[BibT_eX]

[DOI]

Ningning Chen

Proceedings of the Theoretical Aspects of Computing - ICTAC 2022, 2022

A Proof System for Cyber-Physical Systems with Shared-Variable Concurrency.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2022

The Operational and Denotational Semantics of rMECal Calculus for Mobile Edge Computing.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Engineering of Complex Computer Systems, 2022

Denotational and Algebraic Semantics for Cyber-physical Systems.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Engineering of Complex Computer Systems, 2022

Algebraic Semantics for C++11 Memory Model.

[BibT_eX]

[DOI]

Proceedings of the 46th IEEE Annual Computers, Software, and Applications Conferenc, 2022

Formal Analysis and Verification of DPSTM v2 Architecture Using CSP.

[BibT_eX]

[DOI]

Proceedings of the 46th IEEE Annual Computers, Software, and Applications Conferenc, 2022

2021

Language evolution and healthiness for critical cyber-physical systems.

[BibT_eX]

[DOI]

J. Softw. Evol. Process., 2021

A clock-based dynamic logic for schedulability analysis of CCSL specifications.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2021

Formal analysis and automated validation of privacy-preserving AICE protocol in mobile edge computing.

[BibT_eX]

[DOI]

Mob. Networks Appl., 2021

Trace Semantics and Algebraic Laws for Total Store Order Memory Model.

[BibT_eX]

[DOI]

Li-Li Xiao

Qi-Wen Xu

J. Comput. Sci. Technol., 2021

Formalization and Analysis of Ceph Using Process Algebra.

[BibT_eX]

[DOI]

IEICE Trans. Inf. Syst., 2021

A process calculus BigrTiMo of mobile systems and its formal semantics.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2021

Modeling and verifying SDN under Multi-controller architectures using CSP.

[BibT_eX]

[DOI]

Concurr. Comput. Pract. Exp., 2021

Formal Verification of HPS-based Master-Slave Scheme in MEC with Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the 20th IEEE International Conference on Trust, 2021

Formal Modelling and Verification of the RTPS Behavior Module.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Theoretical Aspects of Software Engineering, 2021

A Proof System for HRML with Extended Hoare Logic.

[BibT_eX]

[DOI]

Ningning Chen

Proceedings of the International Symposium on Theoretical Aspects of Software Engineering, 2021

Trace Semantics and Algebraic Laws for MCA ARMv8 Architecture Based on UTP.

[BibT_eX]

[DOI]

Lili Xiao

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2021

Formal Modeling and Verification of ICN-IoT Middleware Architecture (S).

[BibT_eX]

[DOI]

Proceedings of the 33rd International Conference on Software Engineering and Knowledge Engineering, 2021

Formalization and Verification of Dubbo Using CSP.

[BibT_eX]

[DOI]

Zhiru Hou

Proceedings of the 33rd International Conference on Software Engineering and Knowledge Engineering, 2021

Formalization and Verification of Group Communication CoAP Using CSP.

[BibT_eX]

[DOI]

Sini Chen

Proceedings of the Parallel and Distributed Computing, Applications and Technologies, 2021

Modeling and Verifying Ticket-Based Authentication Scheme for IoT Using CSP.

[BibT_eX]

[DOI]

Proceedings of the 2021 IEEE Intl Conf on Parallel & Distributed Processing with Applications, Big Data & Cloud Computing, Sustainable Computing & Communications, Social Computing & Networking (ISPA/BDCloud/SocialCom/SustainCom), New York City, NY, USA, September 30, 2021

Modeling and Verifying Producer-Consumer Communication in Kafka Using CSP.

[BibT_eX]

[DOI]

Proceedings of the ECBS 2021: 7th Conference on the Engineering of Computer Based Systems, 2021

PSTM Transaction Scheduler Verification Based on CSP and Testing.

[BibT_eX]

[DOI]

Proceedings of the ECBS 2021: 7th Conference on the Engineering of Computer Based Systems, 2021

SC4MEC: Automated Implementation of A Secure Hierarchical Calculus for Mobile Edge Computing.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2021

Moded and Continuous Abstract State Machines.

[BibT_eX]

[DOI]

Proceedings of the Logic, Computation and Rigorous Methods, 2021

2020

Modeling and verifying the topology discovery mechanism of OpenFlow controllers in software-defined networks using process algebra.

[BibT_eX]

[DOI]

Marcello M. Bonsangue

Lei Zhang

Sci. Comput. Program., 2020

Formalization and Analysis of Haystack Architecture from Process Algebra Perspective.

[BibT_eX]

[DOI]

Phan Cong Vinh

Mob. Networks Appl., 2020

Security Analysis of the Access Control Solution of NDN Using BAN Logic.

[BibT_eX]

[DOI]

Phan Cong Vinh

Mob. Networks Appl., 2020

Formal analysis and verification of the PSTM architecture using CSP.

[BibT_eX]

[DOI]

J. Syst. Softw., 2020

Specification and Verification of the Zab Protocol with TLA+.

[BibT_eX]

[DOI]

J. Comput. Sci. Technol., 2020

Event-based functional decomposition.

[BibT_eX]

[DOI]

Inf. Comput., 2020

Theoretical and Practical Approaches to the Denotational Semantics for MDESL based on UTP.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2020

Modeling and Analysis of RabbitMQ Using UPPAAL.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE International Conference on Trust, 2020

An Axiomatic Approach to BigrTiMo.

[BibT_eX]

[DOI]

Shengchao Qin

Proceedings of the International Symposium on Theoretical Aspects of Software Engineering, 2020

Modeling and Verifying NDN-based IoV Using CSP.

[BibT_eX]

[DOI]

Proceedings of the 32nd International Conference on Software Engineering and Knowledge Engineering, 2020

Formal Modelling and Verification of MCAC Router Architecture in ICN.

[BibT_eX]

[DOI]

Proceedings of the 32nd International Conference on Software Engineering and Knowledge Engineering, 2020

Formalization and Verification of VANET.

[BibT_eX]

[DOI]

Proceedings of the 32nd International Conference on Software Engineering and Knowledge Engineering, 2020

Modeling and Verifying Data Access Mechanism of NLSR Trust Model.

[BibT_eX]

[DOI]

Proceedings of the 27th Asia-Pacific Software Engineering Conference, 2020

2019

Toward a Unified Executable Formal Automobile OS Kernel and Its Applications.

[BibT_eX]

[DOI]

IEEE Trans. Reliab., 2019

Theoretical and Practical Aspects of Linking Operational and Algebraic Semantics for MDESL.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2019

Isolation Modeling and Analysis Based on Mobility.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2019

Formal Verification of mCWQ Using Extended Hoare Logic.

[BibT_eX]

[DOI]

Mob. Networks Appl., 2019

Modeling and Verifying Basic Modules of Floodlight.

[BibT_eX]

[DOI]

Mob. Networks Appl., 2019

Formalization and Verification of TESAC Using CSP.

[BibT_eX]

[DOI]

Int. J. Softw. Eng. Knowl. Eng., 2019

UTP Semantics of a Calculus for Mobile Ad Hoc Networks.

[BibT_eX]

[DOI]

Proceedings of the Unifying Theories of Programming - 7th International Symposium, 2019

A Logical Approach for the Schedulability Analysis of CCSL.

[BibT_eX]

[DOI]

Proceedings of the 2019 International Symposium on Theoretical Aspects of Software Engineering, 2019

Modeling and Verifying Transaction Scheduling for Software Transactional Memory using CSP.

[BibT_eX]

[DOI]

Proceedings of the 2019 International Symposium on Theoretical Aspects of Software Engineering, 2019

Verifying Opacity of a Modified PSTM.

[BibT_eX]

[DOI]

Yucheng Fang

Proceedings of the 2019 International Symposium on Theoretical Aspects of Software Engineering, 2019

Formalization and Verification of RTPS StatefulWriter Module Using CSP.

[BibT_eX]

[DOI]

Proceedings of the 31st International Conference on Software Engineering and Knowledge Engineering, 2019

Modeling and Verifying TESAC Using CSP.

[BibT_eX]

[DOI]

Proceedings of the 31st International Conference on Software Engineering and Knowledge Engineering, 2019

Verifying Static Aspects of UML models using Prolog (S).

[BibT_eX]

[DOI]

Proceedings of the 31st International Conference on Software Engineering and Knowledge Engineering, 2019

PDNet: A Programming Language for Software-Defined Networks with VLAN.

[BibT_eX]

[DOI]

Shuangqing Xiang

Marcello M. Bonsangue

Proceedings of the Formal Methods and Software Engineering, 2019

A Security Calculus for Wireless Networks of Named Data Networking.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2019

Modeling and Verifying Storm Using CSP.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE International Symposium on High Assurance Systems Engineering, 2019

Modeling and Verifying Spark on YARN Using Process Algebra.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE International Symposium on High Assurance Systems Engineering, 2019

Towards the Mechanized Semantics and Refinement of UML Class Diagrams.

[BibT_eX]

[DOI]

Feng Sheng

Zongyuan Yang

Proceedings of the 26th Asia-Pacific Software Engineering Conference, 2019

2018

Safety Verification of Nonlinear Hybrid Systems Based on Bilinear Programming.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2018

Comparative modelling and verification of Pthreads and Dthreads.

[BibT_eX]

[DOI]

J. Softw. Evol. Process., 2018

Formal analysis of a calculus for WSNs from quality perspective.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2018

Formal Analysis of the PKMv3 Protocol.

[BibT_eX]

[DOI]

Mob. Networks Appl., 2018

Formalization and Verification of the OpenFlow Bundle Mechanism Using CSP.

[BibT_eX]

[DOI]

Int. J. Softw. Eng. Knowl. Eng., 2018

A UTP approach for rTiMo.

[BibT_eX]

[DOI]

Shuangqing Xiang

Formal Aspects Comput., 2018

Modeling and Verifying TopoGuard in OpenFlow-Based Software Defined Networks.

[BibT_eX]

[DOI]

Proceedings of the 2018 International Symposium on Theoretical Aspects of Software Engineering, 2018

Modeling and Verification of NLSR Protocol using UPPAAL.

[BibT_eX]

[DOI]

Xin Li

Proceedings of the 2018 International Symposium on Theoretical Aspects of Software Engineering, 2018

A Fully Abstract Encoding for Sub Asynchronous Pi Calculus.

[BibT_eX]

[DOI]

Wenjun Du

Zhengfeng Yang

Proceedings of the 2018 International Symposium on Theoretical Aspects of Software Engineering, 2018

Security Analysis of the Access Control Solution of NDN Using BAN Logic (S).

[BibT_eX]

[DOI]

Huiwen Wang

Proceedings of the 30th International Conference on Software Engineering and Knowledge Engineering, 2018

Modeling and Verifying Leader Election Algorithm in CSP (S).

[BibT_eX]

[DOI]

Yucheng Fang

Huiwen Wang

Proceedings of the 30th International Conference on Software Engineering and Knowledge Engineering, 2018

Modeling and verifying SDN with multiple controllers.

[BibT_eX]

[DOI]

Lili Xiao

Shuangqing Xiang

Proceedings of the 33rd Annual ACM Symposium on Applied Computing, 2018

UTP Semantics for BigrTiMo.

[BibT_eX]

[DOI]

Shengchao Qin

Proceedings of the Formal Methods and Software Engineering, 2018

Modeling and Verifying NDN Access Control Using CSP.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2018

Assertional Reasoning for Concurrent and Communicating BPEL-like Programs.

[BibT_eX]

[DOI]

Longfei Zhu

Proceedings of the Communication Papers of the 2018 Federated Conference on Computer Science and Information Systems, 2018

Formalization and Verification of Mobile Systems Calculus Using the Rewriting Engine Maude.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE 42nd Annual Computer Software and Applications Conference, 2018

Modeling and Verifying OpenFlow Scheduled Bundle Mechanism Using CSP.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE 42nd Annual Computer Software and Applications Conference, 2018

Modeling and Verifying MooseFS in CSP.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE 42nd Annual Computer Software and Applications Conference, 2018

Modeling and analysis of the disruptor framework in CSP.

[BibT_eX]

[DOI]

Proceedings of the IEEE 8th Annual Computing and Communication Workshop and Conference, 2018

2017

Event-Based Mobility Modeling and Analysis.

[BibT_eX]

[DOI]

ACM Trans. Cyber Phys. Syst., 2017

Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2017

Modeling and Verifying HDFS Using Process Algebra.

[BibT_eX]

[DOI]

Mob. Networks Appl., 2017

RunDroid: recovering execution call graphs for Android applications.

[BibT_eX]

[DOI]

Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, 2017

BigrTiMo-A Process Algebra for Structure-Aware Mobile Systems.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Conference on Engineering of Complex Computer Systems, 2017

A Proof System for MDESL.

[BibT_eX]

[DOI]

Proceedings of the Communication Papers of the 2017 Federated Conference on Computer Science and Information Systems, 2017

Formalization and Verification of the PKMv3 Protocol Using CSP.

[BibT_eX]

[DOI]

Proceedings of the 41st IEEE Annual Computer Software and Applications Conference, 2017

A Proof System for mCWQ.

[BibT_eX]

[DOI]

Proceedings of the 41st IEEE Annual Computer Software and Applications Conference, 2017

Modeling and Analysis of the Security Protocol in C-DAX Based on Process Algebra.

[BibT_eX]

[DOI]

Proceedings of the 41st IEEE Annual Computer Software and Applications Conference, 2017

Assertion-Based Reasoning Method for Calculus of Wireless System.

[BibT_eX]

[DOI]

Luyao Wang

Proceedings of the Models, Algorithms, Logics and Tools, 2017

Modeling and Verifying Identity Authentication Security of HDFS Using CSP.

[BibT_eX]

[DOI]

Chao Xu

Proceedings of the 24th Asia-Pacific Software Engineering Conference, 2017

Formalization and Verification of the PSTM Architecture.

[BibT_eX]

[DOI]

Ailun Liu

Miroslav Popovic

Proceedings of the 24th Asia-Pacific Software Engineering Conference, 2017

2016

Multiphase until formulas over Markov reward models: An algebraic approach.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2016

SMT-Based Symbolic Encoding and Formal Analysis of HML Models.

[BibT_eX]

[DOI]

Mob. Networks Appl., 2016

Developments in concurrent Kleene algebra.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2016

Formalization and analysis of the REST architecture from the process algebra perspective.

[BibT_eX]

[DOI]

Future Gener. Comput. Syst., 2016

An SMT-Based Approach to the Formal Analysis of MARTE/CCSL.

[BibT_eX]

[DOI]

Min Zhang

Frédéric Mallet

Proceedings of the Formal Methods and Software Engineering, 2016

Integrating a Calculus with Mobility and Quality for Wireless Sensor Networks.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE International Symposium on High Assurance Systems Engineering, 2016

Comparative Modeling and Verification of Pthreads and Dthreads.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE International Symposium on High Assurance Systems Engineering, 2016

Shared-Variable Concurrency, Continuous Behaviour and Healthiness for Critical Cyberphysical Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Safety-Critical Systems, 2016

Modeling and Verifying HDFS Using CSP.

[BibT_eX]

[DOI]

Proceedings of the 40th IEEE Annual Computer Software and Applications Conference, 2016

Model-Based Continuous Verification.

[BibT_eX]

[DOI]

Proceedings of the 23rd Asia-Pacific Software Engineering Conference, 2016

2015

Analyzing Event-Based Scheduling in Concurrent Reactive Systems.

[BibT_eX]

[DOI]

ACM Trans. Embed. Comput. Syst., 2015

Core Hybrid Event-B I: Single Hybrid Event-B machines.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2015

Semantic theories of programs with nested interrupts.

[BibT_eX]

[DOI]

Frontiers Comput. Sci., 2015

Denotational semantics and its algebraic derivation for an event-driven system-level language.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2015

Formal Verification of PKMv3 Protocol Using DT-Spin.

[BibT_eX]

[DOI]

Proceedings of the 2015 International Symposium on Theoretical Aspects of Software Engineering, 2015

A SAT-Based Analysis of a Calculus for Wireless Sensor Networks.

[BibT_eX]

[DOI]

Hanne Riis Nielson

Proceedings of the 2015 International Symposium on Theoretical Aspects of Software Engineering, 2015

A Formal Framework for Reasoning Emergent Behaviors in Swarm Robotic Systems.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Engineering of Complex Computer Systems, 2015

Verification for OAuth Using ASLan++.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Symposium on High Assurance Systems Engineering, 2015

A Calculus for Wireless Sensor Networks from Quality Perspective.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Symposium on High Assurance Systems Engineering, 2015

Modeling and Verifying the Ballooning in Xen with CSP.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Symposium on High Assurance Systems Engineering, 2015

Formalization and Verification of REST Architecture in Viewpoints.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Symposium on High Assurance Systems Engineering, 2015

Modeling and Verifying Google File System.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Symposium on High Assurance Systems Engineering, 2015

An Object-Oriented Language for Modeling of Hybrid Systems.

[BibT_eX]

[DOI]

Jianqi Shi

Proceedings of the 16th IEEE International Symposium on High Assurance Systems Engineering, 2015

Probabilistic Analysis of a Calculus for Wireless Sensor Networks.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Safety-Critical Systems, 2015

2014

A Continuous ASM Modelling Approach to Pacemaker Sensing.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2014

Quantitative modelling and analysis of a Chinese smart grid: a stochastic model checking case study.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2014

Formal verification and simulation for platform screen doors and collision avoidance in subway control systems.

[BibT_eX]

[DOI]

Kim Guldstrand Larsen

Alexandre David

Int. J. Softw. Tools Technol. Transf., 2014

Formalizing hybrid systems with Event-B and the Rodin Platform.

[BibT_eX]

[DOI]

Wen Su

Jean-Raymond Abrial

Sci. Comput. Program., 2014

ASM, controller synthesis, and complete refinement.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2014

A formal framework for service mashups with dynamic service selection.

[BibT_eX]

[DOI]

Jianqi Shi

Innov. Syst. Softw. Eng., 2014

Investigating System Survivability from a Probabilistic Perspective.

[BibT_eX]

[DOI]

IEICE Trans. Inf. Syst., 2014

A UTP semantic model for Orc language with execution status and fault handling.

[BibT_eX]

[DOI]

Frontiers Comput. Sci., 2014

Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2014

A Formal Model for a Hybrid Programming Language.

[BibT_eX]

[DOI]

Proceedings of the Unifying Theories of Programming - 5th International Symposium, 2014

Observation-Oriented Semantics for Calculus of Wireless Systems.

[BibT_eX]

[DOI]

Proceedings of the Unifying Theories of Programming - 5th International Symposium, 2014

Modeling and Verifying the TTCAN Protocol Using Timed CSP.

[BibT_eX]

[DOI]

Proceedings of the 2014 Theoretical Aspects of Software Engineering Conference, 2014

Configuration of Services Based on Virtualization.

[BibT_eX]

[DOI]

Proceedings of the 2014 Theoretical Aspects of Software Engineering Conference, 2014

Reasoning about Group-Based Mobility in MANETs.

[BibT_eX]

[DOI]

Proceedings of the 20th IEEE Pacific Rim International Symposium on Dependable Computing, 2014

pIML - An Interrupt Program Modelling Language for Real-Time and Embedded Systems.

[BibT_eX]

[DOI]

Proceedings of the 21st Asia-Pacific Software Engineering Conference, 2014

Developments in Concurrent Kleene Algebra.

[BibT_eX]

[DOI]

Proceedings of the Relational and Algebraic Methods in Computer Science, 2014

2013

Formalization and Verification of REST on HTTP Using CSP.

[BibT_eX]

[DOI]

Proceedings of the Sixth International Workshop on Harnessing Theories for Tool Support for Software, 2013

Modeling and Verification of CAN Bus with Application Layer using UPPAAL.

[BibT_eX]

[DOI]

Proceedings of the Sixth International Workshop on Harnessing Theories for Tool Support for Software, 2013

Apricot - An Object-Oriented Modeling Language for Hybrid Systems

[BibT_eX]

[DOI]

Jianqi Shi

CoRR, 2013

Modeling and verifying the Ariadne protocol using process algebra.

[BibT_eX]

[DOI]

Comput. Sci. Inf. Syst., 2013

A Timing Verification Framework for AUTOSAR OS Component Development Based on Real-Time Maude.

[BibT_eX]

[DOI]

Proceedings of the Seventh International Symposium on Theoretical Aspects of Software Engineering, 2013

Formal Analysis of AODV Using Rely-Guarantee.

[BibT_eX]

[DOI]

Proceedings of the Seventh International Symposium on Theoretical Aspects of Software Engineering, 2013

A Denotational Model for Interrupt-Driven Programs.

[BibT_eX]

[DOI]

Proceedings of the Sixth IEEE International Conference on Software Testing, 2013

Linking Operational Semantics and Algebraic Semantics for Wireless Networks.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2013

Formal Modelling and Analysis of AODV.

[BibT_eX]

[DOI]

Jeff W. Sanders

Proceedings of the 2013 18th International Conference on Engineering of Complex Computer Systems, 2013

Linking Algebraic Semantics and Operational Semantics for Web Services Using Maude.

[BibT_eX]

[DOI]

Proceedings of the 2013 18th International Conference on Engineering of Complex Computer Systems, 2013

Using Daikon to Prioritize and Group Unit Bugs.

[BibT_eX]

[DOI]

Proceedings of the Formal Aspects of Component Software - 10th International Symposium, 2013

Towards a Modeling Language for Cyber-Physical Systems.

[BibT_eX]

[DOI]

Proceedings of the Theories of Programming and Formal Methods, 2013

Linking the Semantics of BPEL Using Maude.

[BibT_eX]

[DOI]

Proceedings of the 20th Asia-Pacific Software Engineering Conference, 2013

2012

Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2012

Modelling Chinese Smart Grid: A Stochastic Model Checking Case Study

[BibT_eX]

[DOI]

CoRR, 2012

Formal Modeling and Analysis of the REST Architecture Using CSP.

[BibT_eX]

[DOI]

Proceedings of the Web Services and Formal Methods - 9th International Workshop, 2012

Denotational Semantics for a Probabilistic Timed Shared-Variable Language.

[BibT_eX]

[DOI]

Proceedings of the Unifying Theories of Programming, 4th International Symposium, 2012

Mechanical Approach to Linking Operational Semantics and Algebraic Semantics for Verilog Using Maude.

[BibT_eX]

[DOI]

Proceedings of the Unifying Theories of Programming, 4th International Symposium, 2012

Unifying Operational Semantics with Algebraic Semantics for Instantaneous Reactions.

[BibT_eX]

[DOI]

Chengcheng Wu

Proceedings of the Unifying Theories of Programming, 4th International Symposium, 2012

Modelling and Analysis of Smart Grid: A Stochastic Model Checking Case Study.

[BibT_eX]

[DOI]

Proceedings of the Sixth International Symposium on Theoretical Aspects of Software Engineering, 2012

Binary Code Level Verification for Interrupt Safety Properties of Real-Time Operating System.

[BibT_eX]

[DOI]

Proceedings of the Sixth International Symposium on Theoretical Aspects of Software Engineering, 2012

Formal Verification and Simulation: Co-verification for Subway Control Systems.

[BibT_eX]

[DOI]

Proceedings of the Sixth International Symposium on Theoretical Aspects of Software Engineering, 2012

The Rely/Guarantee Approach to Verifying Concurrent BPEL Programs.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 10th International Conference, 2012

A Denotational Model for Instantaneous Signal Calculus.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 10th International Conference, 2012

Investigating Time Properties of Interrupt-Driven Programs.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods: Foundations and Applications - 15th Brazilian Symposium, 2012

Complementary Methodologies for Developing Hybrid Systems with Event-B.

[BibT_eX]

[DOI]

Wen Su

Jean-Raymond Abrial

Proceedings of the Formal Methods and Software Engineering, 2012

xBIL - A Hardware Resource Oriented Binary Intermediate Language.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, 2012

ORIENTAIS: Formal Verified OSEK/VDX Real-Time Operating System.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, 2012

Modeling and Verifying the Ariadne Protocol Using CSP.

[BibT_eX]

[DOI]

Proceedings of the IEEE 19th International Conference and Workshops on Engineering of Computer-Based Systems, 2012

Continuous Behaviour in Event-B: A Sketch.

[BibT_eX]

[DOI]

Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012

Continuous ASM, and a Pacemaker Sensing Fragment.

[BibT_eX]

[DOI]

Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012

ASM and Controller Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012

Formalizing Hybrid Systems with Event-B.

[BibT_eX]

[DOI]

Jean-Raymond Abrial

Wen Su

Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012

2011

Algebraic approach to linking the semantics of web services.

[BibT_eX]

[DOI]

Innov. Syst. Softw. Eng., 2011

Formalising the Continuous/Discrete Modeling Step

[BibT_eX]

[DOI]

Proceedings of the Proceedings 15th International Refinement Workshop, 2011

Formalizing Application Programming Interfaces of the OSEK/VDX Operating System Specification.

[BibT_eX]

[DOI]

Proceedings of the 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2011

Modeling and Analyzing the (mu)TESLA Protocol Using CSP.

[BibT_eX]

[DOI]

Proceedings of the 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2011

Towards an Axiomatic Verification System for JavaScript.

[BibT_eX]

[DOI]

Proceedings of the 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2011

Towards a Probabilistic Calculus for Mobile Ad Hoc Networks.

[BibT_eX]

[DOI]

Proceedings of the 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2011

Modeling and Verifying the Code-Level OSEK/VDX Operating System with CSP.

[BibT_eX]

[DOI]

Proceedings of the 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2011

Towards Denotational Semantics for Verilog in PVS.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Conference on Secure Software Integration and Reliability Improvement, 2011

Formal Approaches to Wireless Sensor Networks.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Conference on Secure Software Integration and Reliability Improvement, 2011

From Requirements to Development: Methodology and Example.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2011

A Unifying Approach to Validating Specification-Oriented XML Constraints.

[BibT_eX]

[DOI]

Proceedings of the 13th IEEE International Symposium on High-Assurance Systems Engineering, 2011

Animating the Approach of Deriving Operational Semantics from Algebraic Semantics for Web Services.

[BibT_eX]

[DOI]

Qian Wang

Proceedings of the 13th IEEE International Symposium on High-Assurance Systems Engineering, 2011

A Calculus for Mobile Ad Hoc Networks from a Group Probabilistic Perspective.

[BibT_eX]

[DOI]

Proceedings of the 13th IEEE International Symposium on High-Assurance Systems Engineering, 2011

Formal Approaches to Mode Conversion and Positioning for Vehicle System.

[BibT_eX]

[DOI]

Proceedings of the Workshop Proceedings of the 35th Annual IEEE International Computer Software and Applications Conference, 2011

2010

Web services choreography validation.

[BibT_eX]

[DOI]

Serv. Oriented Comput. Appl., 2010

Linking denotational semantics with operational semantics for web services.

[BibT_eX]

[DOI]

Innov. Syst. Softw. Eng., 2010

Generating Denotational Semantics from Algebraic Semantics for Event-Driven System-Level Language.

[BibT_eX]

[DOI]

Fan Yang

Proceedings of the Unifying Theories of Programming - Third International Symposium, 2010

Towards a Pomset Semantics for a Shared-Variable Parallel Language.

[BibT_eX]

[DOI]

Xu Wang

Proceedings of the Unifying Theories of Programming - Third International Symposium, 2010

A Formal Model for Service Choreography with Exception Handling and Finalization.

[BibT_eX]

[DOI]

Proceedings of the 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2010

Probabilistic Model of System Survivability.

[BibT_eX]

[DOI]

Proceedings of the 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2010

A Denotational Semantical Model for Orc Language.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2010

Formal Approaches to Location Management in Mobile Communications.

[BibT_eX]

[DOI]

Proceedings of the Distributed Computing and Internet Technology, 2010

Formalizing MapReduce with CSP.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, 2010

Formal Modeling and Verifications of Deadlock Prevention Solutions in Web Service Oriented System.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, 2010

2009

PTSC: probability, time and shared-variable concurrency.

[BibT_eX]

[DOI]

Innov. Syst. Softw. Eng., 2009

Modeling MapReduce with CSP.

[BibT_eX]

[DOI]

Proceedings of the TASE 2009, 2009

Formal Approaches to Deadlock Analysis in Competitions of Shared Web Resources.

[BibT_eX]

[DOI]

Proceedings of the TASE 2009, 2009

Animating the Link Between Operational Semantics and Algebraic Semantics for a Probabilistic Timed Shared-Variable Language.

[BibT_eX]

[DOI]

Proceedings of the 33rd Annual IEEE Software Engineering Workshop, 2009

Towards Specification and Refinement of Contracts with Environment Changes.

[BibT_eX]

[DOI]

Proceedings of the 33rd Annual IEEE Software Engineering Workshop, 2009

Formal Approaches to SMS Service Based on Pi Calculus.

[BibT_eX]

[DOI]

Proceedings of the Fourth International Conference on Frontier of Computer Science and Technology, 2009

Formal Modeling and Analyzing Kerberos Protocol.

[BibT_eX]

[DOI]

Proceedings of the CSIE 2009, 2009 WRI World Congress on Computer Science and Information Engineering, March 31, 2009

Locality-Based Normal Form Approach to Linking Algebraic Semantics and Operational Semantics for an Event-Driven System-Level Language.

[BibT_eX]

[DOI]

Proceedings of the 20th Australian Software Engineering Conference (ASWEC 2009), 2009

A Formal Perspective for Service Coordination Framework in Service Oriented Architecture.

[BibT_eX]

[DOI]

Proceedings of the 20th Australian Software Engineering Conference (ASWEC 2009), 2009

2008

From algebraic semantics to denotational semantics for Verilog.

[BibT_eX]

[DOI]

Innov. Syst. Softw. Eng., 2008

Denotational Approach to an Event-Driven System-Level Language.

[BibT_eX]

[DOI]

Proceedings of the Unifying Theories of Programming, Second International Symposium, 2008

ASERE: Assuring the Satisfiability of Sequential Extended Regular Expressions.

[BibT_eX]

[DOI]

Naiyong Jin

Proceedings of the Leveraging Applications of Formal Methods, 2008

An Observational Model for Transactional Calculus of Services Orchestration.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2008

A Denotational Model for Web Services Choreography.

[BibT_eX]

[DOI]

Proceedings of the Distributed Computing and Internet Technology, 2008

Towards the Service Composition Through Buses.

[BibT_eX]

[DOI]

Proceedings of the 11th IEEE High Assurance Systems Engineering Symposium, 2008

Specifying and Verifying Web Transactions.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Networked and Distributed Systems, 2008

Execution Semantics for rCOS.

[BibT_eX]

[DOI]

Proceedings of the 15th Asia-Pacific Software Engineering Conference (APSEC 2008), 2008

2007

A model for BPEL-like languages.

[BibT_eX]

[DOI]

Geguang Pu

Frontiers Comput. Sci. China, 2007

Scalable Formalization of Publish/Subscribe Messaging Scheme Based on Message Brokers.

[BibT_eX]

[DOI]

Proceedings of the Web Services and Formal Methods, 4th International Workshop, 2007

Conformance Validation between Choreography and Orchestration.

[BibT_eX]

[DOI]

Geguang Pu

Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007

An Operational Approach to BPEL-like Programming.

[BibT_eX]

[DOI]

Proceedings of the 31st Annual IEEE / NASA Software Engineering Workshop (SEW-31 2007), 2007

Algebraic Approach to Operational Semantics and Observation-Oriented Semantics for a Timed Shared-Variable Language with Probability.

[BibT_eX]

[DOI]

Proceedings of the 31st Annual IEEE / NASA Software Engineering Workshop (SEW-31 2007), 2007

Looking into Compensable Transactions.

[BibT_eX]

[DOI]

Proceedings of the 31st Annual IEEE / NASA Software Engineering Workshop (SEW-31 2007), 2007

An Inconsistency Free Formalization of B/S Architecture.

[BibT_eX]

[DOI]

Proceedings of the 31st Annual IEEE / NASA Software Engineering Workshop (SEW-31 2007), 2007

Modeling and Verifying Web Services Choreography Using Process Algebra.

[BibT_eX]

[DOI]

Proceedings of the 31st Annual IEEE / NASA Software Engineering Workshop (SEW-31 2007), 2007

Algebraic Semantics for Compensable Transactions.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2007

A Formal Model for Compensable Transactions.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 2007

Unifying Denotational Semantics with Operational Semantics for Web Services.

[BibT_eX]

[DOI]

Proceedings of the Distributed Computing and Internet Technology, 2007

Tool Support for BPEL Verification in ActiveBPEL Engine.

[BibT_eX]

[DOI]

Proceedings of the 18th Australian Software Engineering Conference (ASWEC 2007), 2007

2006

Integrating Probability with Time and Shared-Variable Concurrency.

[BibT_eX]

[DOI]

Proceedings of the 30th Annual IEEE / NASA Software Engineering Workshop (SEW-30 2006), 2006

An Operational Semantics of an Event-Driven System-Level Simulator.

[BibT_eX]

[DOI]

Proceedings of the 30th Annual IEEE / NASA Software Engineering Workshop (SEW-30 2006), 2006

Patterns with Algebraic Properties in BPEL0.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, 2006

Towards the Semantics for Web Service Choreography Description Language.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2006

Theoretical Foundations of Scope-Based Compensable Flow Language for Web Service.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2006

A Denotational Approach to Scope-Based Compensable Flow Language for Web Service.

[BibT_eX]

[DOI]

Geguang Pu

Proceedings of the Advances in Computer Science, 2006

2005

Linking the semantics of a multithreaded discrete event simulation language.

[BibT_eX]

[DOI]

PhD thesis, 2005

2002

Soundness, Completeness and Non-redundancy of Operational Semantics for Verilog Based on Denotational Semantics.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2002

2001

From Operational Semantics to Denotational Semantics for Verilog.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2001

Deriving Operational Semantics from Denotational Semantics for Verilog.

[BibT_eX]

[DOI]

Proceedings of the 8th Asia-Pacific Software Engineering Conference (APSEC 2001), 2001

2000

Formalising VERILOG.

[BibT_eX]

[DOI]