Analysis of the SET e-commerce protocol using a true concurrency process algebra

Considering both qualitative and quantitative aspects in the same modeling approach enhances coherency when analyzing concurrent system properties. Moreover, the impacts of changes related to functional and temporal features are generally better highlighted. In this paper, the authors present their approach to model and analyze behavioral and temporal properties of true concurrency systems. Compared to existing models, the underlying Maximality semantics allows to prune the state space. A specification language is also proposed, extending the LOTOS Process Algebra, in order to support any kind of action durations, like immediate, deterministic, Markovian or arbitrarily distributed ones.

Download Full-text

Refinement of Actions in a Real-Time Process Algebra with a True Concurrency Model

Electronic Notes in Theoretical Computer Science ◽

10.1016/s1571-0661(05)80496-7 ◽

2002 ◽

Vol 70 (3) ◽

pp. 260-280 ◽

Cited By ~ 8

Author(s):

Harald Fecher ◽

Mila Majster-Cederbaum ◽

Jinzhao Wu

Keyword(s):

Real Time ◽

Process Algebra ◽

Time Process ◽

True Concurrency ◽

Concurrency Model

Download Full-text

Twenty Years on: Reflections on the CEDISYS Project. Combining True Concurrency with Process Algebra

Concurrency, Graphs and Models - Lecture Notes in Computer Science ◽

10.1007/978-3-540-68679-8_47 ◽

2008 ◽

pp. 757-777 ◽

Cited By ~ 5

Author(s):

Gérard Boudol ◽

Ilaria Castellani ◽

Matthew Hennessy ◽

Mogens Nielsen ◽

Glynn Winskel

Keyword(s):

Process Algebra ◽

True Concurrency

Download Full-text

Applications of Process Algebra

10.1017/cbo9780511608841 ◽

1990 ◽

Cited By ~ 57

Keyword(s):

Process Algebra

Download Full-text

A Study on Network Service Behavior Verification with Process Algebra and Its Application

Chinese Journal of Computers ◽

10.3724/sp.j.1016.2011.01600 ◽

2011 ◽

Vol 34 (9) ◽

pp. 1660-1668

Author(s):

Fu CHEN ◽

Jia-Hai YANG ◽

Yang YANG ◽

Yuan-Zhuo WANG ◽

Mei-Ying JIA

Keyword(s):

Process Algebra ◽

Network Service ◽

Service Behavior

Download Full-text

Persistent Stochastic Non-Interference

Fundamenta Informaticae ◽

10.3233/fi-2021-2049 ◽

2021 ◽

Vol 181 (1) ◽

pp. 1-35

Author(s):

Jane Hillston ◽

Andrea Marin ◽

Carla Piazza ◽

Sabina Rossi

Keyword(s):

Process Algebra ◽

Operational Semantics ◽

Evaluation Process ◽

Decision Algorithm ◽

Secure Systems ◽

Information Flow Security ◽

Structural Operational Semantics ◽

Timing Properties ◽

Functional Point ◽

Security Property

In this paper, we study an information flow security property for systems specified as terms of a quantitative Markovian process algebra, namely the Performance Evaluation Process Algebra (PEPA). We propose a quantitative extension of the Non-Interference property used to secure systems from the functional point view by assuming that the observers are able to measure also the timing properties of the system, e.g., the response time of certain actions or its throughput. We introduce the notion of Persistent Stochastic Non-Interference (PSNI) based on the idea that every state reachable by a process satisfies a basic Stochastic Non-Interference (SNI) property. The structural operational semantics of PEPA allows us to give two characterizations of PSNI: one based on a bisimulation-like equivalence relation inducing a lumping on the underlying Markov chain, and another one based on unwinding conditions which demand properties of individual actions. These two different characterizations naturally lead to efficient methods for the verification and construction of secure systems. A decision algorithm for PSNI is presented and an application of PSNI to a queueing system is discussed.

Download Full-text