Recommendable!
"Design is an essential part of the development process for many software engineers. Like an architect sketching blueprints, a programmer devises algorithms to support their code and creates models to envision how the different elements of their systems will work together. But what if programmers could test those algorithms and models to uncover design flaws before they could turn into bugs in the written code?
That’s the goal with TLA+, an open-source, high-level language for modeling software programs and hardware systems. Its underlying logic is based on the temporal logic of actions (TLA), a mathematical way to reason about the correctness of concurrent algorithms. Both TLA and TLA+ were developed by Leslie Lamport, a distinguished scientist at Microsoft Research who is best known for inventing LaTeX, a document-preparation system for scientific papers. Lamport also won the 2013 A.M. Turing Award from the Association for Computing Machinery for his work on clarifying the behavior of distributed systems. ...
The language was first used in the industry to model [computer] hardware, particularly at Intel. “It was initially appealing to hardware engineers because [they] were used to the idea of describing things precisely above the circuit level,” says Lamport. ...
Some of today’s tech giants have integrated TLA+ into their development processes. Amazon, for instance, has used TLA+ to test its cloud-computing services, as well as search for hard-to-find yet fundamental algorithm flaws in its distributed systems and optimize performance without sacrificing correctness. Microsoft has applied a similar approach to its Azure cloud-computing platform. Engineers at Oracle have, with the help of TLA+, ensured that their distributed-systems designs are correct."
That’s the goal with TLA+, an open-source, high-level language for modeling software programs and hardware systems. Its underlying logic is based on the temporal logic of actions (TLA), a mathematical way to reason about the correctness of concurrent algorithms. Both TLA and TLA+ were developed by Leslie Lamport, a distinguished scientist at Microsoft Research who is best known for inventing LaTeX, a document-preparation system for scientific papers. Lamport also won the 2013 A.M. Turing Award from the Association for Computing Machinery for his work on clarifying the behavior of distributed systems. ...
This makes TLA+ valuable for verifying that a program’s design or supporting algorithm is valid, a feature made possible by the TLA+ model checker. After creating specifications and writing models on TLA+, engineers can run everything through the model checker to find and fix design errors before they are implemented into code.
Some of today’s tech giants have integrated TLA+ into their development processes. Amazon, for instance, has used TLA+ to test its cloud-computing services, as well as search for hard-to-find yet fundamental algorithm flaws in its distributed systems and optimize performance without sacrificing correctness. Microsoft has applied a similar approach to its Azure cloud-computing platform. Engineers at Oracle have, with the help of TLA+, ensured that their distributed-systems designs are correct."
No comments:
Post a Comment