Towards Verification of Constituent Systems through Automated Proof
This addresses the challenge of ensuring dependable SoS through formal verification of constituent systems, though it appears incremental as an extension of existing tools.
The paper tackles the problem of verifying constituent systems in Systems of Systems (SoS) by developing a proof obligation generator and theorem prover plugin for the Symphony tool platform, using Isabelle/HOL to automatically discharge proof obligations from CML models.
This paper explores verification of constituent systems within the context of the Symphony tool platform for Systems of Systems (SoS). Our SoS modelling language, CML, supports various contractual specification elements, such as state invariants and operation preconditions, which can be used to specify contractual obligations on the constituent systems of a SoS. To support verification of these obligations we have developed a proof obligation generator and theorem prover plugin for Symphony. The latter uses the Isabelle/HOL theorem prover to automatically discharge the proof obligations arising from a CML model. Our hope is that the resulting proofs can then be used to formally verify the conformance of each constituent system, which is turn would result in a dependable SoS.