|
| | | | |
| | | |
| Stat |
Members: 3645
Articles: 2'506'133
Articles rated: 2609
26 April 2024 |
|
| | | | |
|
Article overview
| |
|
|
Verification of Time-Aware Business Processes using Constrained Horn Clauses | | Emanuele De Angelis
; Fabio Fioravanti
; Maria Chiara Meo
; Alberto Pettorossi
; Maurizio Proietti
; | | Date: |
9 Aug 2016 | | Abstract: | We present a method for verifying properties of time-aware business
processes, that is, business process where time constraints on the activities
are explicitly taken into account. Business processes are specified using an
extension of the Business Process Modeling Notation (BPMN) and durations are
defined by constraints over integer numbers. The definition of the operational
semantics is given by a set OpSem of constrained Horn clauses (CHCs). Our
verification method consists of two steps. (Step 1) We specialize OpSem with
respect to a given business process and a given temporal property to be
verified, whereby getting a set of CHCs whose satisfiability is equivalent to
the validity of the given property. (Step 2) We use state-of-the-art solvers
for CHCs to check the satisfiability of such sets of clauses. We have
implemented our verification method using the VeriMAP transformation system,
and the Eldarica and Z3 solvers for CHCs. | | Source: | arXiv, 1608.2807 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser Mozilla/5.0 AppleWebKit/537.36 (KHTML, like Gecko; compatible; ClaudeBot/1.0; +claudebot@anthropic.com)
|
| |
|
|
|
|
News, job offers and information for researchers and scientists:
| |
REGISTER