Formally Specified Model

A Formally Specified Model is a model that is a formal representation that defines system concepts (through formal statements).

• AKA: Formal Specification, Formal Model.
• Context:
  • It can typically perform Specification Functions through formal definitions:
    • Model Input: formal statements, assumptions, constraints
    • Model Output: formal representations, verification results, validation status
    • Model Performance Measure: specification completeness, formal correctness, consistency level
  • ...
  • It can typically define Model Components through formal notation.
  • It can typically specify Model Constraints through formal rules.
  • It can typically maintain Model Consistency through formal verification.
  • It can typically support Model Validation through formal proofs.
  • It can often enable Model Analysis through formal methods.
  • It can often facilitate Model Translation through formal transformations.
  • It can often provide Model Verification through model checking.
  • It can often support Model Evolution through formal refinements.
  • ...
  • It can range from being a Simple Formal Model to being a Complex Formal Model, depending on its specification complexity.
  • It can range from being a Static Model to being a Dynamic Model, depending on its temporal nature.
  • It can range from being a Domain-Specific Model to being a General-Purpose Model, depending on its application scope.
  • It can range from being a Mathematical Model to being a Logical Model, depending on its formalism type.
  • ...
  • It can be based on a Formal Metamodel.
  • It can be expressed in a Formal Language.
  • It can be verified through Model Checking.
  • It can be validated via Formal Verification.
  • ...
• Example(s):
  • Mathematical Models, such as:
    • Algebraic Models, such as:
      • Group Theory Model for abstract algebra.
      • Ring Theory Model for algebraic structures.
    • Statistical Models, such as:
      • Probability Model for uncertainty representation.
      • Distribution Model for data characterization.
  • Logic Models, such as:
    • Predicate Logic Models, such as:
      • First-Order Logic Model for logical reasoning.
      • Modal Logic Model for possibility representation.
    • Temporal Logic Models, such as:
      • Linear Temporal Logic Model for sequential behavior.
      • Branching Time Logic Model for concurrent behavior.
  • Semantic Models, such as:
    • Ontological Models, such as:
      • Domain Ontology Model for knowledge representation.
      • Upper Ontology Model for concept hierarchy.
    • Behavioral Models, such as:
      • State Machine Model for system behavior.
      • Process Algebra Model for interaction patterns.
  • ...
• Counter-Example(s):
  • Informal Models, which lack formal definitions.
  • Natural Language Descriptions, which lack formal semantics.
  • Controlled Vocabularys, which lack formal relationships.
• See: Formal Method, Model Theory, Formal Language, Specification Language, Verification Method, Algorithm, Model Checking Task, TLA+.

---

---

References

2002

• (Chella et al., 2002) ⇒ Antonio Chella, Massimo Cossentino, Roberto Pirrone, and Andrea Ruisi. (2002). “Modeling Ontologies for Robotic Environments.” In: Proceedings of the 14th International Conference on Software Engineering and Knowledge Engineering. doi:10.1145/568760.568775
  • An Ontology can be defined as a formally specified model of bodies of knowledge defining the concepts used to describe a domain and the relations that hold between them.

2001

• (Miller & Mukerji, 2001) ⇒ Joaquin Miller and Jishnu Mukerji. (2001). “Model Driven Architecture (MDA): A Draft with annotations of issues to resolve Architecture Board ORMSC." Object Management Group
  • A formally specified model is useful because:
    • It facilitates creation of compatible platform specific models/specifications corresponding to the same platform-independent model and hence implementations that are easier to bridge together.
    • It provides a common reference model and vocabulary with unambiguous meaning thus reducing the chances of miscommunication among system designers and builders.
    • It facilitates standardization of more precisely specified designs and patterns, thus allowing for portability of design, and makes it easier to support interoperability among different realizations of the same design on different platforms.

---