ACIMS/M&S Net Meeting

Tucson, Arizona

December 5, 2003

 

What follows are notes arising from an afternoon meeting of the above group. The meeting explored possible synergies between Formal Methods (rigorous mathematics) and Modeling and Simulation.

 

1.      Pendulum example.

-        Initial effort to explore potential compatabilities between formal methods and modeling and simulation.

-        Initial driving force was to use such an exploration as a discussion topic for the FM component of Foundations 2004.

-        Having a common example would allow for FM and M&S researchers to better understand potential synergies.

2.      Combining DEVS and Logic.

-        Timing issues.

-        Modularity.

-        RAP (Reactive Action Planning; Jim Firby and Steve Fitzgerald)

3.      DEVS:

-        Analysis and synthesis

-        Use of logic to determine invariance and/or show properties of DEVS models

4.      Why?

-        Reasoning easier in logic than in systems theory.

-        Complexity: ameliorated by abstraction, algebra.

-        Cannot readily do formal proof: validate versus verify.

-        Use of logic to demonstrate “sanity” properties of DEVS models.

-        Need to give formal semantics to the various components of DEVS. With the semantics, and associated logic, can then reason about DEVS models. Can take a constrained view on properties For example, focusing on timing. Analysis could be both off-line and on-line.

-        Experimental frames. Context within which a model can be used. Capture assumptions and objectives. Composability, reuse and patterns (approaches, roles), multi-concepts.

-        How and legitimacy of model/frame

-        Formalization: capturing the objectives, assumptions and constraints

-        Matching: verifying objectives, assumptions and constrains satisfaction.

-        Lotrec prover (from Toulouse).

-        Large and non-linear systems.

-        Dynamically defined pattern recognition.

-        Emergent behavior. Unexpected or unintended results arising from a system?

-        Distributed simulation and completeness of HLA.

-        Componentization and use of logic to describe constraints on linking.

-        Interaction dynamics.

-        Ontologies.

-        Formal methods as a tool for making inferences. Co-running of simulator and real-system. Possibly using the simulator to help optimize the system. Some kind of data mining.

5.      Dollars:

-        New NSF call with regards to simulation. Uncertainty. ITR. February 24th, 2004.

-        New software engineering approaches.

 

Dan Craigen

December 5, 2003