# Huibiao Zhu

According to our database

Collaborative distances:

^{1}, Huibiao Zhu authored at least 175 papers between 2001 and 2019.Collaborative distances:

## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### On csauthors.net:

## Bibliography

2019

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

IEEE Trans. Reliability, 2019

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

ACM Trans. Softw. Eng. Methodol., 2019

Isolation Modeling and Analysis Based on Mobility.

ACM Trans. Softw. Eng. Methodol., 2019

Formal Verification of mCWQ Using Extended Hoare Logic.

MONET, 2019

Modeling and Verifying Basic Modules of Floodlight.

MONET, 2019

Formalization and Verification of RTPS StatefulWriter Module Using CSP.

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

Modeling and Verifying TESAC Using CSP.

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

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

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

Modeling and Verifying Storm Using CSP.

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

Modeling and Verifying Spark on YARN Using Process Algebra.

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

2018

Safety Verification of Nonlinear Hybrid Systems Based on Bilinear Programming.

IEEE Trans. on CAD of Integrated Circuits and Systems, 2018

Comparative modelling and verification of Pthreads and Dthreads.

Journal of Software: Evolution and Process, 2018

Formal analysis of a calculus for WSNs from quality perspective.

Sci. Comput. Program., 2018

Formal Analysis of the PKMv3 Protocol.

MONET, 2018

Formalization and Verification of the OpenFlow Bundle Mechanism Using CSP.

International Journal of Software Engineering and Knowledge Engineering, 2018

A UTP approach for rTiMo.

Formal Asp. Comput., 2018

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

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

Modeling and Verification of NLSR Protocol using UPPAAL.

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

A Fully Abstract Encoding for Sub Asynchronous Pi Calculus.

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

Formalization and Verification of the OpenFlow Bundle Mechanism Using CSP.

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

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

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

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

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

Modeling and verifying SDN with multiple controllers.

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

UTP Semantics for BigrTiMo.

Proceedings of the Formal Methods and Software Engineering, 2018

Modeling and Verifying NDN Access Control Using CSP.

Proceedings of the Formal Methods and Software Engineering, 2018

Assertional Reasoning for Concurrent and Communicating BPEL-like Programs.

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.

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

Modeling and Verifying OpenFlow Scheduled Bundle Mechanism Using CSP.

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

Modeling and Verifying MooseFS in CSP.

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

2017

Event-Based Mobility Modeling and Analysis.

TCPS, 2017

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

Sci. Comput. Program., 2017

Modeling and Verifying HDFS Using Process Algebra.

MONET, 2017

RunDroid: recovering execution call graphs for Android applications.

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

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

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

A Proof System for MDESL.

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.

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

A Proof System for mCWQ.

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.

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

Assertion-Based Reasoning Method for Calculus of Wireless System.

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

Modeling and Verifying Identity Authentication Security of HDFS Using CSP.

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

Formalization and Verification of the PSTM Architecture.

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

2016

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

Theor. Comput. Sci., 2016

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

MONET, 2016

Developments in concurrent Kleene algebra.

J. Log. Algebr. Meth. Program., 2016

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

Future Generation Comp. Syst., 2016

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

Proceedings of the Formal Methods and Software Engineering, 2016

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

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

Comparative Modeling and Verification of Pthreads and Dthreads.

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

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

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

Modeling and Verifying HDFS Using CSP.

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

Model-Based Continuous Verification.

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

2015

Analyzing Event-Based Scheduling in Concurrent Reactive Systems.

ACM Trans. Embedded Comput. Syst., 2015

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

Sci. Comput. Program., 2015

Semantic theories of programs with nested interrupts.

Frontiers Comput. Sci., 2015

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

Formal Asp. Comput., 2015

Formal Verification of PKMv3 Protocol Using DT-Spin.

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

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

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

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

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

Verification for OAuth Using ASLan++.

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

A Calculus for Wireless Sensor Networks from Quality Perspective.

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

Modeling and Verifying the Ballooning in Xen with CSP.

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

Formalization and Verification of REST Architecture in Viewpoints.

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

Modeling and Verifying Google File System.

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

An Object-Oriented Language for Modeling of Hybrid Systems.

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

Probabilistic Analysis of a Calculus for Wireless Sensor Networks.

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

2014

A Continuous ASM Modelling Approach to Pacemaker Sensing.

ACM Trans. Softw. Eng. Methodol., 2014

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

STTT, 2014

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

STTT, 2014

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

Sci. Comput. Program., 2014

ASM, controller synthesis, and complete refinement.

Sci. Comput. Program., 2014

A formal framework for service mashups with dynamic service selection.

ISSE, 2014

Investigating System Survivability from a Probabilistic Perspective.

IEICE Transactions, 2014

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

Frontiers Comput. Sci., 2014

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

Formal Asp. Comput., 2014

Formalization and Verification of REST on HTTP Using CSP.

Electr. Notes Theor. Comput. Sci., 2014

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

Electr. Notes Theor. Comput. Sci., 2014

A Formal Model for a Hybrid Programming Language.

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

Observation-Oriented Semantics for Calculus of Wireless Systems.

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

Modeling and Verifying the TTCAN Protocol Using Timed CSP.

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

Configuration of Services Based on Virtualization.

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

Reasoning about Group-Based Mobility in MANETs.

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.

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

Developments in Concurrent Kleene Algebra.

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

2013

Modeling and verifying the Ariadne protocol using process algebra.

Comput. Sci. Inf. Syst., 2013

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

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

Formal Analysis of AODV Using Rely-Guarantee.

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

A Denotational Model for Interrupt-Driven Programs.

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

Linking Operational Semantics and Algebraic Semantics for Wireless Networks.

Proceedings of the Formal Methods and Software Engineering, 2013

Formal Modelling and Analysis of AODV.

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.

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

Using Daikon to Prioritize and Group Unit Bugs.

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

Towards a Modeling Language for Cyber-Physical Systems.

Proceedings of the Theories of Programming and Formal Methods, 2013

Linking the Semantics of BPEL Using Maude.

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

2012

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

J. Log. Algebr. Program., 2012

Formal Modeling and Analysis of the REST Architecture Using CSP.

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

Denotational Semantics for a Probabilistic Timed Shared-Variable Language.

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

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

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

Unifying Operational Semantics with Algebraic Semantics for Instantaneous Reactions.

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

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

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.

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

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

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

The Rely/Guarantee Approach to Verifying Concurrent BPEL Programs.

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

A Denotational Model for Instantaneous Signal Calculus.

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

Investigating Time Properties of Interrupt-Driven Programs.

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

Complementary Methodologies for Developing Hybrid Systems with Event-B.

Proceedings of the Formal Methods and Software Engineering, 2012

xBIL - A Hardware Resource Oriented Binary Intermediate Language.

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

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

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

Modeling and Verifying the Ariadne Protocol Using CSP.

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

Continuous Behaviour in Event-B: A Sketch.

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

Continuous ASM, and a Pacemaker Sensing Fragment.

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

ASM and Controller Synthesis.

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

Formalizing Hybrid Systems with Event-B.

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

2011

Formalising the Continuous/Discrete Modeling Step

Proceedings of the Proceedings 15th International Refinement Workshop, 2011

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

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

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

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

Towards an Axiomatic Verification System for JavaScript.

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

Towards a Probabilistic Calculus for Mobile Ad Hoc Networks.

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

Towards Denotational Semantics for Verilog in PVS.

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

Formal Approaches to Wireless Sensor Networks.

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

From Requirements to Development: Methodology and Example.

Proceedings of the Formal Methods and Software Engineering, 2011

A Unifying Approach to Validating Specification-Oriented XML Constraints.

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.

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.

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

Formal Approaches to Mode Conversion and Positioning for Vehicle System.

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

2010

Web services choreography validation.

Service Oriented Computing and Applications, 2010

Linking denotational semantics with operational semantics for web services.

ISSE, 2010

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

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

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

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

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

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

Probabilistic Model of System Survivability.

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

A Denotational Semantical Model for Orc Language.

Proceedings of the Theoretical Aspects of Computing, 2010

Formal Approaches to Location Management in Mobile Communications.

Proceedings of the Distributed Computing and Internet Technology, 2010

Formalizing MapReduce with CSP.

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.

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.

ISSE, 2009

Modeling MapReduce with CSP.

Proceedings of the TASE 2009, 2009

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

Proceedings of the TASE 2009, 2009

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

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

Towards Specification and Refinement of Contracts with Environment Changes.

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

Formal Approaches to SMS Service Based on Pi Calculus.

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

Formal Modeling and Analyzing Kerberos Protocol.

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.

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

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

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

2008

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

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

ASERE: Assuring the Satisfiability of Sequential Extended Regular Expressions.

Proceedings of the Leveraging Applications of Formal Methods, 2008

An Observational Model for Transactional Calculus of Services Orchestration.

Proceedings of the Theoretical Aspects of Computing, 2008

A Denotational Model for Web Services Choreography.

Proceedings of the Distributed Computing and Internet Technology, 2008

Towards the Service Composition Through Buses.

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

Specifying and Verifying Web Transactions.

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

Execution Semantics for rCOS.

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

2007

A model for BPEL-like languages.

Frontiers Comput. Sci. China, 2007

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

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

Conformance Validation between Choreography and Orchestration.

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

An Operational Approach to BPEL-like Programming.

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.

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

Looking into Compensable Transactions.

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

An Inconsistency Free Formalization of B/S Architecture.

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

Modeling and Verifying Web Services Choreography Using Process Algebra.

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

Algebraic Approach to Linking the Semantics of Web Services.

Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007

Algebraic Semantics for Compensable Transactions.

Proceedings of the Theoretical Aspects of Computing, 2007

A Formal Model for Compensable Transactions.

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

Unifying Denotational Semantics with Operational Semantics for Web Services.

Proceedings of the Distributed Computing and Internet Technology, 2007

Tool Support for BPEL Verification in ActiveBPEL Engine.

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

2006

Integrating Probability with Time and Shared-Variable Concurrency.

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

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

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

Patterns with Algebraic Properties in BPEL0.

Proceedings of the Leveraging Applications of Formal Methods, 2006

Towards the Semantics for Web Service Choreography Description Language.

Proceedings of the Formal Methods and Software Engineering, 2006

From Algebraic Semantics to Denotational Semantics for Verilog.

Proceedings of the 11th International Conference on Engineering of Complex Computer Systems (ICECCS 2006), 2006

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

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

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

Proceedings of the Advances in Computer Science, 2006

2005

Linking the semantics of a multithreaded discrete event simulation language.

PhD thesis, 2005

2002

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

Proceedings of the Formal Methods and Software Engineering, 2002

2001

From Operational Semantics to Denotational Semantics for Verilog.

Proceedings of the Correct Hardware Design and Verification Methods, 2001

Deriving Operational Semantics from Denotational Semantics for Verilog.

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