Dynamic Specification in the Responsive and Formal Desig

This research enhances the Responsive and Formal Design process by showing how an algebraic structure with its operation and an extracted theory (logic) of the system behavior can be used to capture the dynamism of a system as it responds to state-transitioning actions. Formal methods like model checking and theorem proving may then be applied to the logic to maintain correctness, consistency, and traceability in the system design.;A flexible, reliable, and risk-tolerant specification and design methodology is needed to produce good quality engineered systems. Towards this end, the Responsive and Formal Design process emphasizes the use of models and formal methods early in the design phases.;The RFD process has the goal of being a model-based systems engineering specification and design methodology that will reduce design time and cost and improve correctness and confidence through formal verification in a flexible, risk-tolerant manner. The high level mathematical concept used by the RFD to represent its elements and their interaction is category theory. Category theory is a form of abstract mathematics that represents phenomena as objects and morphisms -- relations between objects. (Information) Channel theory uses category theory to reason about the flow of information in systems.;The primary object in channel theory is a classification (or a classification table); it consists of columns representing situation features and rows representing different situations that can be realized in a given system. A dynamic information channel consists of classifications corresponding to both the functional components of a system and their actions, and infomorphisms (mappings) between the components (the "parts") and the core (the "whole") representing a system-wide view.;The RFD uses static classifications of information channel theory to represent the static behavior of a system. In constructing a computational model of dynamic behavior, I introduce an algebraic structure formed from a relation on the types of a classification to define the actions of components of a system. Complementing the structure is a logical operation applied to the classification table to specify how the system evolves.;Intrinsic to a classification is a theory consisting of logical constraints that summarize the behavior captured by the classification. The constraints are interpreted as conditional statements of truth about the system defined by the classifications. In this work, I also devise an algorithm for extracting a theory of a system from a representation of its dynamic behavior.