Using Heterogeneous Formal Methods in Model-Based Development
Abstract:
Different modeling formalisms and analysis tools are often used to represent the variety of concerns that need to be addressed when designing complex cyber-physical systems. The way information and inferences from these heterogeneous perspectives is combined is often ad hoc and informal. This presentation concerns the formal foundations for using heterogeneous formal methods based on behavioral semantics. We consider abstraction, compositional reasoning and system-level inferences all within a framework that supports the use of arbitrary formalisms to model and analyze any particular aspect or component of a system. We also illustrate an approach for using theorem proving tools to establish constraints for lower level control system design.