Abstract
Business processes usually have to consider certain con-
straints like domain specific and quality requirements. The
automated formal verification of these constraints is de-
sirable, but requires the user to provide an unambiguous
formal specification. In particular since the notations for
business process modeling are usually visual flow-oriented
languages, the notational gap to the languages usually em-
ployed for the formal specification of constraints, e.g., tem-
poral logic, is significant and hard to bridge. Thus, our ap-
proach relies on UML Activities as a single language for
the specification of both business processes and the cor-
responding constraints. For the expression of such con-
straints, we have provided a process pattern definition lan-
guage based on specialized Activities. In this paper, we de-
scribe how model checking can be employed for formal ver-
ification of business processes against such patterns. For
this, we present an automated transformation of the busi-
ness process and the corresponding patterns into a transi-
tion system and temporal logic, respectively.
straints like domain specific and quality requirements. The
automated formal verification of these constraints is de-
sirable, but requires the user to provide an unambiguous
formal specification. In particular since the notations for
business process modeling are usually visual flow-oriented
languages, the notational gap to the languages usually em-
ployed for the formal specification of constraints, e.g., tem-
poral logic, is significant and hard to bridge. Thus, our ap-
proach relies on UML Activities as a single language for
the specification of both business processes and the cor-
responding constraints. For the expression of such con-
straints, we have provided a process pattern definition lan-
guage based on specialized Activities. In this paper, we de-
scribe how model checking can be employed for formal ver-
ification of business processes against such patterns. For
this, we present an automated transformation of the busi-
ness process and the corresponding patterns into a transi-
tion system and temporal logic, respectively.
| Original language | English |
|---|---|
| Title of host publication | First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007 |
| Publisher | IEEE Computer Society Press |
| Publication status | Published - 2007 |
| Event | Finds and Results from the Swedish Cyprus Expedition: A Gender Perspective at the Medelhavsmuseet - Stockholm, Sweden Duration: 21 Sep 2009 → 25 Sep 2009 |
Conference
| Conference | Finds and Results from the Swedish Cyprus Expedition: A Gender Perspective at the Medelhavsmuseet |
|---|---|
| Country/Territory | Sweden |
| City | Stockholm |
| Period | 21/09/09 → 25/09/09 |
Keywords
- business processes
- visual languages
- temporal logic