{"entities":{"Q1085970":{"pageid":1096722,"ns":120,"title":"Item:Q1085970","lastrevid":66284241,"modified":"2026-04-12T08:46:43Z","type":"item","id":"Q1085970","labels":{"en":{"language":"en","value":"Proof rules for fault tolerant distributed programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3984554"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085970$90FA7D34-57CD-4CF2-A9F0-2448D434877F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"48e78df826dbfb11ea23d48ba0ce3ca031890d95","datavalue":{"value":{"text":"Proof rules for fault tolerant distributed programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1085970$4CE4D2CB-EDB8-4D4D-AB0A-CD4E6705B62D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0ea3c05efd99ab7871066fc94f3925fa1b67754b","datavalue":{"value":"0608.68016","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1085970$FC4F465F-CAFD-4F04-99EE-EFB2692A1030","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0bd39e89f477b950184786fef1c6794de981ba6b","datavalue":{"value":"10.1016/0167-6423(87)90003-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1085970$DD44DD99-94C2-4A65-AE06-B50808D7E883","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ef3979302b875c048dc5c989eccf025415e00902","datavalue":{"value":{"entity-type":"item","numeric-id":757078,"id":"Q757078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085970$2BE49E5B-BD98-4AA6-9DF4-88211CB7A072","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"587def83e79f97beefcdeb871c90b592319b633b","datavalue":{"value":{"entity-type":"item","numeric-id":1060001,"id":"Q1060001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085970$164D3CA2-81DF-49F4-9202-44BB27D09CA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"97ed3b0664441e8d880d927898de01db2ab18f95","datavalue":{"value":{"entity-type":"item","numeric-id":796291,"id":"Q796291"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085970$FACB3AEA-34F1-404D-BBE8-8ADC58CC8437","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4082512e7d3530b9726df691c7c28e9fec542a8c","datavalue":{"value":{"entity-type":"item","numeric-id":169675,"id":"Q169675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085970$180AB09F-12D5-4443-8EAE-14565D7A2FB9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ae48c61eed19d1e1e1f33f9255d5b329362d064","datavalue":{"value":{"time":"+1987-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1085970$1248A355-AF4A-47E1-A5CE-2A28892ECCD0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"50cf2670825b24f0e94abde1b48cdcf940860990","datavalue":{"value":"https://hdl.handle.net/1813/6482","type":"string"},"datatype":"url"},"type":"statement","id":"Q1085970$A6569978-7323-4A15-AC23-DE21F5B89115","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b2a0cacff554268f93ced0ad53d8526e8925ea53","datavalue":{"value":"Proving the properties of a program which must execute on a distributed system whose nodes may fail is a complex task. Such proofs must take into account the effects of hardware failures at all possible points in the execution of individual processes. The difficulty in accomplishing this is compounded by the need to cater also for the simultaneous failure of two or more processing nodes. In this paper, we consider programs written in a version of Hoare's CSP and define a set of axioms and inference rules by which proofs can be constructed in three steps: proving the properties of each process when its communicants are prone to failure, establishing the effects of failure of each process, and combining these two steps to determine the fault tolerant properties of the whole program. The proof system is thus compositional, in the sense that proofs can be constructed in a modular way.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085970$E32F7150-1254-42D9-87D4-01584A979010","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec3769495799f08479987ac368adf64f125a2b66","datavalue":{"value":"68N25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1085970$1D4D3453-A9D9-4BC8-B16C-B28BD033D02C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1085970$1D80813C-07CB-48D7-A2EB-8A5095106B4D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"40fcbb8d33be236be0be37febf30be921da4fc48","datavalue":{"value":"3984554","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1085970$74C68EE0-64C6-4F0E-8593-A0EE628A4FDC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e225ac4aec700ae2c67cab0cb7802b0627e7a3da","datavalue":{"value":"distributed system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085970$98B78526-C624-4B69-A87A-EB7F14C421EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fd7d4d2d84c6100ad0a94e78a2fcd8c88cc1b993","datavalue":{"value":"hardware failures","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085970$B4E9390C-18F2-4E93-B077-860FE79B723C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"899df1d6f7201757340f58f279c981c8a9b4f0e1","datavalue":{"value":"processing nodes","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085970$A5994C7F-8732-4E06-9BC0-311607BA47B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4c8710feba3ac62faea4a8522baa0c66e6b134ff","datavalue":{"value":"Hoare's CSP","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085970$6BE68F11-6809-46AA-A221-E024AD995827","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9ddf481075a308929d086d398b952c77f9d345b1","datavalue":{"value":"fault tolerant properties","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085970$DC1BA6C5-2C26-409D-9C68-41947989D818","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"14a0dd3e1b83404196449aa90cc83aae915af1cf","datavalue":{"value":"proof system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085970$270CF3B5-4831-4BF0-8891-769658554091","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085970$EA2F2BD3-C5B8-435E-8E4F-E3FDF196956D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"095be718ac44fa6516a789b9ac6130315bcb888f","datavalue":{"value":"W2000257907","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1085970$8A980B8B-7036-4B45-8B4F-C579E47E06C5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7398da6ad48566bdaeec82532921db68f08c6d6b","datavalue":{"value":{"entity-type":"item","numeric-id":1330425,"id":"Q1330425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"60749b00473f5c1d8b805b7689e7715cf170ba75","datavalue":{"value":{"amount":"+0.8166846036911011","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1085970$09F71895-8ACC-47C1-9EED-F08BF462776E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5460c3c4115d038ac07973252e2a76e86093dad7","datavalue":{"value":{"entity-type":"item","numeric-id":3681909,"id":"Q3681909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"60749b00473f5c1d8b805b7689e7715cf170ba75","datavalue":{"value":{"amount":"+0.8166846036911011","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1085970$BAA4FAE5-BD97-4183-949A-FDF7D3BA89EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5e1408a7200fdecd35eb35c2d5c4fe04cabdcee9","datavalue":{"value":{"entity-type":"item","numeric-id":3316570,"id":"Q3316570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7feaa672c5f8fdc3d547755e7d2f64d2b54784d","datavalue":{"value":{"amount":"+0.8018232583999634","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1085970$AF5423F1-D22B-4E3C-8880-4E0E661A362E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eee4294e71cb3b66235c64fdb14d02d42c0ec26b","datavalue":{"value":{"entity-type":"item","numeric-id":4560363,"id":"Q4560363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb62d6f33899ebfae2555677363a6f148bdda243","datavalue":{"value":{"amount":"+0.7740575671195984","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1085970$640EE85C-BA27-483B-9198-7A4CBF71E3F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7d7045f2d31c534448bdcd51e9fe2bbe8f64104","datavalue":{"value":{"entity-type":"item","numeric-id":757079,"id":"Q757079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07687b757389cb43af147ab039c2a1ef2f4fcb23","datavalue":{"value":{"amount":"+0.7685841917991638","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1085970$9713D7E7-AF57-47CC-A77B-AB4F83B981BF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof rules for fault tolerant distributed programs","badges":[]}}}}}