%0 Journal Article %1 Daszczuk16 %A Daszczuk, Wiktor B. %D 2016 %I Oxford University Press %J The Computer Journal %K checking, citas, citeulike model, pendiente, referencias %R 10.1093/comjnl/bxw099 %T Communication and Resource Deadlock Analysis Using IMDS Formalism and Model Checking %U http://dx.doi.org/10.1093/comjnl/bxw099 %X Modern static deadlock detection techniques deal with the global properties of the verified systems, using methods that explore the state space. Local features, like partial deadlocks or individual process terminations, are not easily expressed or checked by such methods. Also the distinction between communication deadlocks and resource deadlocks, common in dynamic waits-for methods, cannot be addressed or verified by static methods. An Integrated Model of Distributed Systems (IMDS) is proposed which specifies distributed systems as sets of servers' states, sets of messages and sets of actions. The message passing/resource sharing dualism of distributed systems is provided by projections: on servers (server view) and on agents (agent view), yet the uniform specification of a verified system is preserved. A progress of computation is defined in terms of actions which change (local) states and generate messages.

@article{Daszczuk16, abstract = {{Modern static deadlock detection techniques deal with the global properties of the verified systems, using methods that explore the state space. Local features, like partial deadlocks or individual process terminations, are not easily expressed or checked by such methods. Also the distinction between communication deadlocks and resource deadlocks, common in dynamic waits-for methods, cannot be addressed or verified by static methods. An Integrated Model of Distributed Systems (IMDS) is proposed which specifies distributed systems as sets of servers' states, sets of messages and sets of actions. The message passing/resource sharing dualism of distributed systems is provided by projections: on servers (server view) and on agents (agent view), yet the uniform specification of a verified system is preserved. A progress of computation is defined in terms of actions which change (local) states and generate messages.}}, added-at = {2017-09-08T10:52:59.000+0200}, author = {Daszczuk, Wiktor B.}, biburl = {https://www.bibsonomy.org/bibtex/2f5d9a306c5b983e1e8cc5d5c9f09595b/fernand0}, citeulike-article-id = {14245912}, citeulike-linkout-0 = {http://dx.doi.org/10.1093/comjnl/bxw099}, citeulike-linkout-1 = {http://comjnl.oxfordjournals.org/content/early/2016/12/18/comjnl.bxw099.abstract}, citeulike-linkout-2 = {http://comjnl.oxfordjournals.org/content/early/2016/12/18/comjnl.bxw099.full.pdf}, day = 20, doi = {10.1093/comjnl/bxw099}, interhash = {664e215fbfcac5c1c1f7004d43eb2930}, intrahash = {f5d9a306c5b983e1e8cc5d5c9f09595b}, issn = {1460-2067}, journal = {The Computer Journal}, keywords = {checking, citas, citeulike model, pendiente, referencias}, month = dec, posted-at = {2017-01-03 16:23:50}, priority = {2}, publisher = {Oxford University Press}, timestamp = {2017-09-08T10:53:23.000+0200}, title = {{Communication and Resource Deadlock Analysis Using IMDS Formalism and Model Checking}}, url = {http://dx.doi.org/10.1093/comjnl/bxw099}, year = 2016 }