{"id":328,"date":"2015-02-17T09:23:05","date_gmt":"2015-02-17T09:23:05","guid":{"rendered":"http:\/\/www.etfos.unios.hr\/ijeces-test\/?p=328"},"modified":"2017-03-23T08:04:48","modified_gmt":"2017-03-23T08:04:48","slug":"logical-consistency-validation-tools-for-distributed-systems","status":"publish","type":"post","link":"http:\/\/www.etfos.unios.hr\/ijeces\/vol-4-no-1-2013\/logical-consistency-validation-tools-for-distributed-systems\/","title":{"rendered":"Logical Consistency Validation Tools for Distributed Systems"},"content":{"rendered":"<div  class=\"fusion-fullwidth fullwidth-box hundred-percent-fullwidth\"  style='background-color: rgba(255,255,255,0);background-position: center center;background-repeat: no-repeat;padding-top:0px;padding-right:0px;padding-bottom:0px;padding-left:0px;'><div class=\"fusion-builder-row fusion-row \"><div  class=\"fusion-layout-column fusion_builder_column fusion_builder_column_1_1  fusion-one-full fusion-column-first fusion-column-last fusion-column-no-min-height 1_1\"  style='margin-top:0px;margin-bottom:0px;'>\n\t\t\t<div class=\"fusion-column-wrapper\" style=\"background-position:left top;background-repeat:no-repeat;-webkit-background-size:cover;-moz-background-size:cover;-o-background-size:cover;background-size:cover;\"  data-bg-url=\"\">\n\t\t\t\t<div class=\"fusion-title title fusion-title-size-three\" style=\"margin-top:0px;margin-bottom:31px;\"><h3 class=\"title-heading-left\">Drago \u017dagar, Nino Vrande\u010di\u0107, Antun Stoi\u0107<\/h3><div class=\"title-sep-container\"><div class=\"title-sep sep-single sep-solid\" style=\"border-color:#1e73be;\"><\/div><\/div><\/div><div class=\"fusion-sep-clear\"><\/div><div class=\"fusion-separator fusion-full-width-sep sep-single sep-dashed\" style=\"border-color:#1e73be;border-top-width:1px;margin-left: auto;margin-right: auto;margin-top:;margin-bottom:10px;\"><\/div><div data-canvas-width=\"600.915\"><strong>Abstract<\/strong><\/div>\n<div data-canvas-width=\"600.915\">As a result of using Information Technology (IT) in different technological processes it is necessary to develop new application specific communication protocols. The number of application specific protocols is growing rapidly in different areas: medicine, communication, industry, power systems, computer networks, etc. Protocol errors discovered in the implementation phase are usually a consequence of inconsistent protocol design, which implies the necessity of methodology for error detection in an early design phase. This paper describes formal methods for distributed systems, especially SPIN\/Promela tool for formal verification of logical consistency in distributed systems. A protocol used in power systems IEC60870-5-101 has been verified as an example of formal verification of a distributed system. Formal specification, simulation and verification of logical consistency have been successfully done by using SPIN\/Promela software.<\/div>\n<div class=\"fusion-sep-clear\"><\/div><div class=\"fusion-separator fusion-full-width-sep sep-single sep-dashed\" style=\"border-color:#1e73be;border-top-width:1px;margin-left: auto;margin-right: auto;margin-top:10px;margin-bottom:10px;\"><\/div><div data-canvas-width=\"70\"><strong>Keywords<\/strong><\/div>\n<div data-canvas-width=\"403.605\">distributed systems, finite state machine, protocol, validation<\/div>\n<div class=\"fusion-sep-clear\"><\/div><div class=\"fusion-separator fusion-full-width-sep sep-single sep-dashed\" style=\"border-color:#1e73be;border-top-width:1px;margin-left: auto;margin-right: auto;margin-top:10px;margin-bottom:10px;\"><\/div><p><a href=\"http:\/\/www.etfos.unios.hr\/ijeces\/wp-content\/uploads\/pappers\/ijeces_vol_4_no_1_01.pdf\" target=\"_blank\"><\/p>\n<div class=\"alignleft\"><i class=\"fa fontawesome-icon fa-file-text-o circle-yes\" style=\"border-color:#ffffff;background-color:#1e73be;font-size:15.84px;line-height:31.68px;height:31.68px;width:31.68px;margin-right:9px;color:#ffffff;\"><\/i><\/div><p><\/a><\/p>\n<div class=\"fusion-clearfix\"><\/div>\n\n\t\t\t<\/div>\n\t\t<\/div><\/div><\/div>\n","protected":false},"excerpt":{"rendered":"","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[42],"tags":[],"_links":{"self":[{"href":"http:\/\/www.etfos.unios.hr\/ijeces\/wp-json\/wp\/v2\/posts\/328"}],"collection":[{"href":"http:\/\/www.etfos.unios.hr\/ijeces\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.etfos.unios.hr\/ijeces\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.etfos.unios.hr\/ijeces\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"http:\/\/www.etfos.unios.hr\/ijeces\/wp-json\/wp\/v2\/comments?post=328"}],"version-history":[{"count":3,"href":"http:\/\/www.etfos.unios.hr\/ijeces\/wp-json\/wp\/v2\/posts\/328\/revisions"}],"predecessor-version":[{"id":1145,"href":"http:\/\/www.etfos.unios.hr\/ijeces\/wp-json\/wp\/v2\/posts\/328\/revisions\/1145"}],"wp:attachment":[{"href":"http:\/\/www.etfos.unios.hr\/ijeces\/wp-json\/wp\/v2\/media?parent=328"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.etfos.unios.hr\/ijeces\/wp-json\/wp\/v2\/categories?post=328"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.etfos.unios.hr\/ijeces\/wp-json\/wp\/v2\/tags?post=328"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}