Integrating formal methods by unifying abstractions

Abstract

Integrating formal methods enhances their power as an intellectual tool in modelling and design. This holds regardless of automation, but a fortiori if software tools are conceived in an integrated framework. Among the many approaches to integration, most valuable are those with the widest potential impact and least obsolescence or dependency on technology or particular tool-oriented paradigms. From a practical view, integration by unifying models leads to more uniform, wider-spectrum, yet simpler language design in automated tools for formal methods. Hence this paper shows abstractions that cut across levels and boundaries between disciplines, help unifying the growing diversity of aspects now covered by separate formal methods and mathematical models, and even bridge the gap between "continuous" and "discrete" systems. The abstractions also yield conceptual simplification by hiding non-essential differences, avoiding repeating the same theory in different guises. The underlying framework, not being the main topic, is outlined quite tersely, but enough for showing the preferred formalism to express and reason about the abstract paradigms of interest. Three such paradigms are presented in sufficient detail to appreciate the surprisingly wide scope of the obtained unification. The function extension paradigm is useful from signal processing to functional predicate calculus. The function tolerance paradigm spans the spectrum from analog filters to record types, relational databases and XML semantics. The coordinate space paradigm covers modelling issues ranging from transmission lines to formal semantics, stochatic processes and temporal calculi. One conclusion is that integrated formal methods are best served by calculational tools.