engleski

Scenario Modeling and Verification for Business Processes

In this paper we describe modeling for verification of business process with Spin model checker. Our primary goal is the development of Promela language description for e–invoice web service. Modeling for verification follows Church’s synthesis problem: for input scenario “dataflow” model, output is Promela model. Sequence of model transformations translates the scenario into the Promela language code. At the end whole process is illustrated with e–invoice web service example.

scenarios ; model checking ; model transformation ; Spin model checker ; model driven engineering ; interworking formal methods ; finite automaton

nije evidentirano