A Formal Framework for Specifying and Verifying Microservices Based Process Flows

被引：19

作者：

Camilli, Matteo ^{[1
]}

Bellettini, Carlo ^{[1
]}

Capra, Lorenzo ^{[1
]}

Monga, Mattia ^{[1
]}

机构：

[1] Univ Milan, Dept Comp Sci, Milan, Italy

来源：

SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2017 | 2018年 / 10729卷

关键词：

Microservices; Orchestration; Formal methods; Petri nets; Verification; Time analysis; SESSION TYPES; ORCHESTRATION; REQUIREMENTS; SEMANTICS; BPEL;

D O I：

10.1007/978-3-319-74781-1_14

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

The microservices architectural style is changing the way in which software is perceived, conceived and designed. Thus, there is a call for techniques and tools supporting the problem of specifying and verifying communication behavior of microservice systems. We present a formal semantics based on Petri nets for microservices based process flows specified using the CONDUCTOR orchestration language: a JSON-based domain specific language designed by Netflix, Inc. We give a formal semantics in terms of a translation from CONDUCTOR specifications into Time Basic Petri net models, i.e., Petri nets supporting the definition of temporal constraints. The Petri net model can be used for computer aided verification purposes by means of well-known techniques implemented by powerful, off-the-shelf model checking tools.

引用

页码：187 / 202

页数：16

共 29 条

[1] MODEL-CHECKING IN DENSE REAL-TIME [J].

ALUR, R ;

COURCOUBETIS, C ;

DILL, D .

INFORMATION AND COMPUTATION, 1993, 104 (01) :2-34

[2]

Alur R., 1990, Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science (90CH2897-7), P414, DOI 10.1109/LICS.1990.113766

[3]

[Anonymous], 2016, NETFL COND MICR ORCH

[4] Reachability Analysis of Time Basic Petri Nets: a Time Coverage Approach [J].

Bellettini, Carlo ;

Capra, Lorenzo .

13TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC 2011), 2012, :110-117

[5]

Bellettini C, 2013, LECT NOTES COMPUT SC, V8169, P83, DOI 10.1007/978-3-642-41036-9_9

[6] Timed automata: Semantics, algorithms and tools [J].

Bengtsson, J ;

Yi, W .

LECTURES ON CONCURRENCY AND PETRI NETS: ADVANCES IN PETRI NETS, 2004, 3098 :87-124

[7] Multiparty Session Types Within a Canonical Binary Theory, and Beyond [J].

Caires, Luis ;

Perez, Jorge A. .

FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS (FORTE 2016), 2016, 9688 :74-95

[8]

Caires L, 2010, LECT NOTES COMPUT SC, V6269, P222, DOI 10.1007/978-3-642-15375-4_16

[9]

Camilli Matteo, 2016, 2016 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), P165, DOI 10.1109/SYNASC.2016.036

[10] Event-Based Runtime Verification of Temporal Properties Using Time Basic Petri Nets [J].

Camilli, Matteo ;

Gargantini, Angelo ;

Scandurra, Patrizia ;

Bellettini, Carlo .

NASA FORMAL METHODS (NFM 2017), 2017, 10227 :115-130

← 1 2 3 →