The Verification of a Distributed System.
The article discusses the verification and validation of distributed systems. Particular focus is given to partial failure and asynchrony. Details on formal specification languages such as TLA+ and Coq, and on the formal verification method known as model checking, are presented. Informal methods su...
| Published in: | Communications of the ACM Vol. 59; no. 2; pp. 52 - 56 |
|---|---|
| Main Author: | |
| Format: | Article |
| Published: |
Association for Computing Machinery
Feb2016
|
| Subjects: | |
| Online Access: | View this record in EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=112719412&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 112719412 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Feb2016 vid: 59 iid: 2 pid: 68 pub: Association for Computing Machinery artinfo: ui: 112719412 10.1145/2844108 ppf: 52 ppct: 4 formats: tig: atl: The Verification of a Distributed System. aug: au: MCCAFFREY, CAITIE affil: Tech lead for observability at Twitter. su: Distributed computing Software verification Software validation Computer software testing Technical specifications sug: subj: Distributed computing Software verification Software validation Computer software testing Technical specifications ab: The article discusses the verification and validation of distributed systems. Particular focus is given to partial failure and asynchrony. Details on formal specification languages such as TLA+ and Coq, and on the formal verification method known as model checking, are presented. Informal methods such as monitoring, canary tests, and unit and integration tests are also discussed, along with random model checkers and fault-injection testing. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2016 holdings: @attributes: islocal: N |
|---|