Abstract | ||
---|---|---|
Controllability for service models is a similar criterion as soundness for workflow models: it establishes a necessary condition for correct behavior of a given service model. Technically, controllability is the problem to decide, for a given service, whether it can interact correctly with at least one other service. Parameters to the problem are the established correctness criterion (e.g. deadlock freedom, livelock freedom, quasi-liveness), the shape of partners (centralized partners versus independently acting partners), or the shape of communication (asynchronous versus synchronous). In this article, we survey and partly extend various recent results concerning the verification of controllability for Petri net based service models. Significant extensions include the study of livelock freedom as correctness criterion as well as the new results on autonomous multi-port controllability. |
Year | DOI | Venue |
---|---|---|
2009 | 10.1007/978-3-642-00899-3_9 | T. Petri Nets and Other Models of Concurrency |
Keywords | Field | DocType |
centralized partner,correctness criterion,established correctness criterion,deadlock freedom,livelock freedom,correct behavior,necessary condition,autonomous multi-port controllability,service model,similar criterion | Transition system,Asynchronous communication,Petri net,Controllability,Computer science,Correctness,Deadlock,Soundness,Workflow,Distributed computing | Journal |
Volume | ISSN | Citations |
2 | 0302-9743 | 53 |
PageRank | References | Authors |
2.05 | 23 | 1 |
Name | Order | Citations | PageRank |
---|---|---|---|
Karsten Wolf | 1 | 757 | 42.53 |