Proceedings Second Workshop on Formal Aspects of Virtual Organisations (2010)
Bryans, Jeremy, Fitzgerald, John
FAVO2009 was the second workshop on Formal Aspects of Virtual Organisations. The purpose of the FAVO workshops is to encourage an active community of researchers and practitioners using formal...
Security implications of structure ⋆ (2008)
Computer security is an important issue in determining the dependability of computer systems. It becomes even more crucial when we talk about computer-based systems (CBS), where we take into...
A failures semantics for ET-LOTOS (2007)
Steve Schneider, Royal Holloway, Jeremy Bryans, Jim Davies
A denotational semantics is presented for ET-LOTOS [LeL94] in the style of semantics for timed CSP, in terms of timed failures with additional information about internal events. This semantics is...
Reasoning about XACML policies using CSP (2005)
Using Csp, Jeremy Bryans, Jeremy Bryans, Jeremy Bryans
In this work we explore the use of process algebra in formalising and analysing access control policies. We do this by considering a standard access control language (XACML) and show how the core...
Modelling Opacity using Petri Nets (2004)
Jeremy Bryans, Jeremy Bryans, Maciej Koutny, Maciej Koutny, Peter Y. A. Ryan, Peter Y. A. Ryan
We consider opacity as a property of the local states of the secure (or high-level) part of the system, based on the observation of the local states of a low-level part of the system as well as...
Implementing a modal logic over data and processes using XTL (2001)
Jeremy Bryans, Carron Shankland
Abstract The modal logic FULL is designed to capture strong bisimulation over early symbolic transition systems (STSs) for full LOTOS. It provides a compact way of expressing and verifying properties...
Stochastic Model Checking for Multimedia (2000)
Bryans, Jeremy, Bowman, Howard, Derrick, John
Modern distributed systems include a class of applications in which non-functional requirements are important. In particular, these applications include multimedia facilities where real time...
A model checking algorithm for stochastic systems (2000)
Jeremy Bryans, Howard Bowman, John Derrick
In this report we present an algorithm for model-checking stochastic automata with respect to a probabilistic temporal logic. We consider the stochastic automata presented in [D'A99]. In...
Model checking stochastic automata (2000)
Jeremy Bryans, Howard Bowman, John Derrick
Modern distributed systems include a class of applications in which non-functional requirements are important. In particular, these applications include multimedia facilities where real time...
Stochastic Specification and Verification (1999)
Modern distributed systems include a class of applications in which non-functional requirements are important. In particular, these applications include multimedia facilities where real time...
Constraint Orientated Specification with CSP and Real Time Temporal Logic (1998)
this paper we propose such a specification framework, which allows the specifier a choice of two languages: Communicating Sequential Processes (CSP) [Hoa85] and a version of Propositional Temporal...
Using Probability to Reason about Soft Deadlines (1998)
. Soft deadlines are significant in systems in which a bound on the response time is important, but the failure to meet the response time is not a disaster. Soft deadlines occur, for example, in...
CSP, PVS and a Recursive Authentication Protocol (1997)
Jeremy Bryans, Steve Schneider
this paper we consider the nature of machine proofs used in the CSP approach to the verification of authentication protocols. In [Sch96], a general method is presented for the analysis and...
Towards a denotational semantics for ET-LOTOS (1995)
Jeremy Bryans, Jim Davies, Steve Schneider
The formal specification language LOTOS is an international standard for use in Open Systems Interconnection. A timed extension called ET-LOTOS has been proposed. This paper presents a fully-abstract...
Real-time CSP and ET-LOTOS (1995)
Jeremy Bryans, Jim Davies, Steve Schneider
This paper is intended to support and stimulate discussion at the COST 247 meeting in Brighton, 19th and 20th July 1994. It begins with a comprehensive introduction to the language of real-time CSP....
Real-time LOTOS and timed observations (1995)
Jim Davies, Jeremy Bryans, Steve Schneider
This paper presents a new semantic model for real-time LOTOS, based upon a notion of timed observations. The novelty of the model is explained, as is its value. It di#ers from the usual operational...
J. Bryans, J. Fitzgerald, A. Romanovsky, A. Roth, Jeremy Bryans, John Fitzgerald, ...
Distributed information systems are critical to the functioning of many businesses; designing them to be dependable is a challenging but important task. We report our experience in using formal...
Added entries UNIVERSITY OF NEWCASTLE UPON TYNE (1054)
J. Bryans, J. Fitzgerald, Jeremy Bryans, John Fitzgerald, J. Bryans, J. Fitzgerald
Managing the evolution of a dynamic virtual organisation (VO) is a considerable challenge, particularly in ensuring that participating agents provide sufficient access to resources in order to...