Using Category Theory to Verify Implementation Against Design in Concurrent Systems | Zendy

Ming Zhu | Zendy; Peter Grogono | Zendy; Olga Ormandjieva | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Using Category Theory to Verify Implementation Against Design in Concurrent Systems

Author(s) -

Ming Zhu,

Peter Grogono,

Olga Ormandjieva

Publication year - 2015

Publication title -

procedia computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.334

H-Index - 76

ISSN - 1877-0509

DOI - 10.1016/j.procs.2015.05.030

Subject(s) - computer science , consistency (knowledge bases) , programming language , process (computing) , communicating sequential processes , process calculus , concurrent engineering , erasmus+ , formal methods , software engineering , semantics (computer science) , artificial intelligence , operational semantics , art , process integration , the renaissance , process engineering , engineering , art history

The research has shown that process-oriented programming languages provide a suitable means for developing concurrent systems. However, in the development of a concurrent system, there is a challenge to manage consistency between design and implementation. To deal with such a challenge, we propose a new formal verification methodology and illustrate it by a running example. In this methodology, a concurrent system is designed using a process algebra, namely communicating sequential processes, and implemented in a process-oriented programming language, namely Erasmus. The consistency between the design and the implementation of such a concurrent system is verified formally using category theory

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research