A UTP approach for rTiMo
type: Item
instance of: scholarly article
title: A UTP approach for rTiMo
zbMATH Open document ID: 1425.68304
author: Wanling Xie
author: Shuangqing Xiang
author: Huibiao Zhu
published in: Formal Aspects of Computing
publication date: 2018-11-16T00:00:00Z
Mathematics Subject Classification ID: 68Q85
Mathematics Subject Classification ID: 68Q55
zbMATH DE Number: 6980317
zbMATH Keywords: rTiMo
zbMATH Keywords: mobile systems
zbMATH Keywords: UTP semantics
zbMATH Keywords: Hoare logic
describes a project that uses: Isabelle
describes a project that uses: Maria
MaRDI profile type: Publication
full work available at URL: s00165-018-0467-1
OpenAlex ID: W2885842066
cites work: Verification of sequential and concurrent programs
cites work: A Hoare logic for linear systems
cites work: A model checking-based approach for security policy verification of mobile systems
cites work: Mobile ambients
cites work: Timed mobility in process algebra and Petri nets
cites work: Strategy based semantics for mobility with time and access permissions
cites work: Modular state space analysis of coloured Petri Nets
cites work: Modular Analysis of Petri Nets
cites work: The safety-critical Java memory model formalised
cites work: A Hoare logic for dynamic networks of asynchronously communicating deterministic processes
cites work: An algebraic approach to the design of compilers for object-oriented languages
cites work: Metrics for labelled Markov processes
cites work: A New Roadmap for Linking Theories of Programming
cites work: Q3997501
cites work: From algebra to operational semantics
cites work: Laws of programming
cites work: Normal form approach to compiler design
cites work: An axiomatic basis for computer programming
cites work: Q3777424
cites work: Unifying Semantics for Concurrent Programming
cites work: Extending Hoare logic to real-time
cites work: Probabilistic models for the guarded command language
cites work: In praise of algebra
cites work: Developments in concurrent Kleene algebra
cites work: Reasoning about actions with loops via Hoare logic
cites work: Formal Techniques for Networked and Distributed Systems - FORTE 2005
cites work: Modelling Mobile IP with Mobile Petri Nets
cites work: Q3045275
cites work: A calculus of communicating systems
cites work: Q4248252
cites work: Abstraction, Refinement and Proof for Probabilistic Systems
cites work: Resources, concurrency, and local reasoning
cites work: Isabelle. A generic theorem prover
cites work: A structural approach to operational semantics
cites work: Q4287490
cites work: Q3922134
cites work: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
cites work: A lattice-theoretical fixpoint theorem and its applications
cites work: Hoare logic for Java in Isabelle/HOL
cites work: Q4201911
cites work: UTP Semantics for rTiMo
cites work: Q4787253
cites work: Denotational semantics and its algebraic derivation for an event-driven system-level language
cites work: Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language
DOI: 10.1007/S00165-018-0467-1
description: scientific article; zbMATH DE number 6980317