Mathematical/Formal Modeling Of Observed ASM Inputs

[josh]

Note that adding additional claims about real inequalities does not invalidate any of the existing claims which do not reference those assumptions. It does allow for a) a wider range of specification that is important in practice, and b) easier construction of accuracy bounds for discrete automata simulation of pheonomena that is described by differential equations or other continuous formalisms – i.e. along the lines of standard numerical methods practice, developing simultaneous lower & upper bounds on the accuracy of an approximation.

[josh]

I read some papers on the ASM formalism decades ago. There the main thrust of research was improvement of refinement based & abstraction based semantic models of software programs.

Independently, informal systems of specification like UML diagramming focused on using systems of states & transitions to convey domain & program models.

Software engineers & scholars of formal methods pushed the ASM system to add simulators, theorem provers, model checkers, etc.

When the state transition networks are viewed as software machines, then the view is procedural & Hoare Logic naturally applies.

Today, the synthesis that is exciting is combining ez, intuitive, partly visual interfaces to domain & software specification with super powered tools for reasoning about the specifications & their entailments, testing those against expectations & various formal properties, & using the executable artifacts as precision inputs into powerful metaprogramming libraries, languages, & IDEs.

In what sense is this sort of “software spec” called “complete”? There can be many factors:
a) The spec reifies all relevant specification claims in ways that make the entailments precise.
b) The spec translates to language & diagrams that relevant parties can view in understandable pieces & affirm or dispute
c) We can conduct arbitrarily complete sampling of dynamic states & transitions to check, at the relevant level of detail, that the systems described are what was conceived of & intended.
d) We can automate procedures that will either
i. yield an optimized software implementation or
ii. describe which chunks of software spec still need an implementation or
iii. declare that the larger world system is currently incapable of deriving an implementation which satisfies all of the constraints, focusing on the region of failure.

This is stronger performance than what alternative systems of specification achieve in practice.

iv. The level & nature of assurance for the implementation of each bit of specification is a hidden set of parameters. What is appropriate & what is possible & what is affordable or too expensive varies widely across types of demands. Where refinement proof is appropriate & relevant, it could be incorporated as a demand. This is unlikely to be an impact gesture in practice. Better, in practical reality, is extremely comprehensive verification of unit tests (often offered as a default).

[josh]

In general, if our model includes N semi-independent “processes”/forms, we can have a few different kinds of theoretical models for how they coordinate or don’t (complete independence of event times) and, for completeness, different models of how that can “real” model be simulated for various testing purposes.

[Author]

Posts