2019/05/30 by Diego Calvanese, Silvio Ghilardi, Calvanese, Diego +7
Business, Management and Accounting · Computer Science · Engineering · #Business Process Modeling and Analysis #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Safety Systems Engineering in Autonomy #Service-Oriented Architecture and Web Services
paper · pdf · doi:10.48550/arxiv.1905.12991
openalex publication_date 2019/05/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We propose DAB -- a data-aware extension of the BPMN de-facto standard with\nthe ability of operating over case and persistent data (partitioned into a\nread-only catalog and a read-write repository), and that balances between\nexpressiveness and the possibility of supporting parameterized verification of\nsafety properties on top of it. In particular, we take inspiration from the\nliterature on verification of artifact systems, and consider verification\nproblems where safety properties are checked irrespectively of the content of\nthe read-only catalog, possibly considering an unbounded number of active cases\nand tuples in the catalog and repository. Such problems are tackled using fully\nimplemented array-based backward reachability techniques belonging to the\nwell-established tradition of SMT model checking. We also identify relevant\nclasses of DABs for which the backward reachability procedure implemented in\nthe MCMT array-based model checker is sound and complete, and then further\nstrengthen such classes to ensure termination.\n