Using First-Order Logic to Reason about Submodule Construction

We consider the following problem: For a system consisting of two components, the behavior of one component is known as well as the desired global behavior. What should be the behavior of the second component such that the behavior of the composition of the two conforms to the desired behavior ? - This problem has been called "submodule construction" or "equation solving"; and in the context of supervisory control, it is the problem of designing a suitable controller (second component) which controls a given system to be controlled (first component). Solutions to this problem have been described in the context of various specification formalisms and various conformance relations. This paper presents a new formulation of this problem and its solution in first-order logic. It is also shown how the solutions for submodule construction in various specification formalisms can be derived from the solution in logic. The simple proof of correctness for the logic solution is...

• Type: Journal
• Year: 2009
• Where: FORTE
• Authors: Gregor von Bochmann
• Keywords: Formal Methods, FORTE 2009, Solutions, Specification Formalisms, Various Specification Formalisms