Verification of Deployed Artifact Systems via Data Abstraction

被引：0

作者：

Belardinelli, Francesco ^{[1
]}

Lomuscio, Alessio ^{[1
]}

Patrizi, Fabio ^{[1
]}

机构：

[1] Univ London Imperial Coll Sci Technol & Med, Dept Comp, London SW7 2AZ, England

来源：

SERVICE-ORIENTED COMPUTING | 2011年 / 7084卷

基金：

英国工程与自然科学研究理事会;

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Artifact systems are a novel paradigm for specifying and implementing business processes described in terms of interacting modules called artifacts. Artifacts consist of data and lifecycle models, accounting for the relational structure of the artifact state and its possible evolutions over time. We consider the problem of verifying artifact systems against specifications expressed in quantified temporal logic. This problem is in general undecidable. However, when artifact systems are deployed, their states can contain only a bounded number of elements. We exploit this fact to develop an abstraction technique that enables us to verify deployed artifact systems by model checking their bounded abstraction.

引用

页码：142 / 156

页数：15

共 50 条

[31] Data Abstraction: A General Framework to Handle Program Verification of Data Structures
Braine, Julien
Gonnord, Laure
Monniaux, David
[J]. STATIC ANALYSIS, SAS 2021, 2021, 12913 : 215 - 235
[32] Verification and behavior abstraction towards a tractable verification technique for large distributed systems
Nitsche, U
[J]. JOURNAL OF SYSTEMS AND SOFTWARE, 1996, 33 (03) : 273 - 285
[33] Parameterised Verification of Stabilisation Properties via Conditional Spotlight Abstraction
Timm, Nils
Gruner, Stefan
[J]. FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS (FTSCS 2016), 2017, 694 : 145 - 160
[34] Neural Policy Safety Verification via Predicate Abstraction: CEGAR
Vinzent, Marcel
Sharma, Siddhant
Hoffmann, Joerg
[J]. THIRTY-SEVENTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, VOL 37 NO 12, 2023, : 15188 - 15196
[35] Automatic data path abstraction for verification of large scale designs
Paruthi, V
Mansouri, N
Vemuri, R
[J]. INTERNATIONAL CONFERENCE ON COMPUTER DESIGN: VLSI IN COMPUTERS AND PROCESSORS, PROCEEDINGS, 1998, : 192 - 194
[36] Artifact Systems with Data Dependencies and Arithmetic
Damaggio, Elio
Deutsch, Alin
Vianu, Victor
[J]. ACM TRANSACTIONS ON DATABASE SYSTEMS, 2012, 37 (03):
[37] Standard artifact for the geometric verification of terrestrial laser scanning systems
Gonzalez-Jorge, H.
Riveiro, B.
Armesto, J.
Arias, P.
[J]. OPTICS AND LASER TECHNOLOGY, 2011, 43 (07): : 1249 - 1256
[38] Abstraction of graph transformation systems by temporal logic and its verification
Yamamoto, Mitsuharu
Tanabe, Yoshinori
Takahashi, Koichi
Hagiya, Masami
[J]. VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2008, 4171 : 518 - +
[39] Verification of Artifact-Centric Systems: Decidability and Modeling Issues
Solomakhin, Dmitry
Montali, Marco
Tessaris, Sergio
De Masellis, Riccardo
[J]. SERVICE-ORIENTED COMPUTING, ICSOC 2013, 2013, 8274 : 252 - 266
[40] An efficient approach for abstraction-refinement verification of hybrid systems
Liu, Baoluo
Pei, Hailong
Zhang, Shengxiang
Li, Jiangqiang
[J]. 2007 IEEE INTERNATIONAL CONFERENCE ON CONTROL AND AUTOMATION, VOLS 1-7, 2007, : 333 - 338

← 1 2 3 4 5 →