On Hoare Triples Applicability to Dependable System Specification Synthesis
Vadym Viktorovych Shkarupylo, Alexander Chemeris, В.В. Душеба, Равіль Камілович Кудерметов, Аndrii Oliinyk · 2020
Modern level of dependable systems engineering process organization is tightly interwoven with formal methods application. Those are typically the model checkers, bringing in the automation. Despite the significant developments in this direction, the aspect of formal specifications synthesis automation is still lagging behind. To this end, a technique is proposed, covering the aspects of diminishing the breach between the analytical interpretation of formal specification and its implementation on the basis of the formalism chosen. The technique is grounded on Communicating Sequential Processes calculus, Hoare triples and Temporal Logic of Actions. To prove the technique proposed, a case study, demonstrating the Message Queuing Telemetry Transport protocol specification synthesis, has been conducted.