作者: Karsten Wolf
DOI: 10.1007/978-3-642-00899-3_9
关键词: Computer science 、 Distributed computing 、 Service (business) 、 Correctness 、 Controllability 、 Asynchronous communication 、 Deadlock 、 Transition system 、 Soundness 、 Petri net
摘要: Controllability for service models is a similar criterion as soundness workflow models: it establishes necessary condition correct behavior of given model. Technically, controllability the problem to decide, service, whether can interact correctly with at least one other service. Parameters are established correctness (e.g. deadlock freedom, livelock quasi-liveness), shape partners (centralized versus independently acting partners), or communication (asynchronous synchronous). In this article, we survey and partly extend various recent results concerning verification Petri net based models. Significant extensions include study freedom well new on autonomous multi-port controllability.