A UTP approach for rTiMo

DOI10.1007/S00165-018-0467-1MaRDI QIDQ1624596zbMATH OpenOpenAlexFDO

Authors Wanling Xie, Shuangqing Xiang, Huibiao Zhu

Publication date 16 November 2018

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-018-0467-1

zbMATH Keywords

Hoare logicmobile systemsrTiMoUTP semantics

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• UTP semantics for rTiMo
• Timed mobility in process algebra and Petri nets
• Formal Methods for the Design of Real-Time Systems
• Extending timed mobility with probabilities and real-time
• Strategy based semantics for mobility with time and access permissions

Cites work

• scientific article; zbMATH DE number 2088675 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3735102 (Why is no real title available?)
• scientific article; zbMATH DE number 48630 (Why is no real title available?)
• scientific article; zbMATH DE number 400814 (Why is no real title available?)
• scientific article; zbMATH DE number 1296290 (Why is no real title available?)
• scientific article; zbMATH DE number 549971 (Why is no real title available?)
• scientific article; zbMATH DE number 1852174 (Why is no real title available?)
• A Hoare logic for dynamic networks of asynchronously communicating deterministic processes
• A Hoare logic for linear systems
• A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
• A calculus of communicating systems
• A lattice-theoretical fixpoint theorem and its applications
• A model checking-based approach for security policy verification of mobile systems
• A new roadmap for linking theories of programming
• A structural approach to operational semantics
• Abstraction, Refinement and Proof for Probabilistic Systems
• An algebraic approach to the design of compilers for object-oriented languages
• An axiomatic basis for computer programming
• Denotational semantics and its algebraic derivation for an event-driven system-level language
• Developments in concurrent Kleene algebra
• Extending Hoare logic to real-time
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• From algebra to operational semantics
• Hoare logic for Java in Isabelle/HOL
• In praise of algebra
• Isabelle. A generic theorem prover
• Laws of programming
• Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language
• Metrics for labelled Markov processes
• Mobile ambients
• Modelling mobile IP with mobile Petri nets
• Modular Analysis of Petri Nets
• Modular state space analysis of coloured Petri nets
• Normal form approach to compiler design
• Probabilistic models for the guarded command language
• Reasoning about actions with loops via Hoare logic
• Resources, concurrency, and local reasoning
• Strategy based semantics for mobility with time and access permissions
• The safety-critical Java memory model formalised
• Timed mobility in process algebra and Petri nets
• UTP semantics for rTiMo
• Unifying Semantics for Concurrent Programming
• Verification of sequential and concurrent programs

Cited in

(8)

• Three Approaches to Timed External Choice in UTP
• Domain Analysis and Description – Sorts, Types, Intents
• A process calculus BigrTiMo of mobile systems and its formal semantics
• Extending timed mobility with probabilities and real-time
• UTP semantics for rTiMo
• Domain modelling: a foundation for software development
• Angelic processes for CSP via the UTP
• Theoretical and practical approaches to the denotational semantics for MDESL based on UTP

Describes a project that uses

Uses Software

• Isabelle
• Maria

This page was built for publication: A UTP approach for rTiMo

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1624596)