modelverse/techreport/general/axioms.tex

\chapter{Axioms}
\label{chap:axioms}
We define a set of requirements for a Modelverse.
These requirements, or axioms, will be used during our formalization to motivate our decisions.
Although implementation-related requirements are not needed for our formalization, they are mentioned as it is something every implementation should conform to.

After an explanation of what each axiom represents, we give an overview of how all these axioms are related to each other.

\section{\axiomForeverRunning}
The Modelverse should always be able to continue running.
As such, no modifications to the behaviour should require a restart, except for changes to the (minimal) kernel (and thus the action language semantics).
An (authorized) user should be able to alter all core concepts, with changes automatically applied for all connected Modelverse Interfaces.

Forever running also implies that the Modelverse runs as a service, separate from the MvI program, which is used by the user, but also on a different machine.
A more drastic interpretation is that it should be parallelized and distributed, as to cope with possible hardware failure.
We do not require this more drastic interpretation, though it is certainly a feature to take into account in an implementation evaluation.

The forever running does not apply to the MvI, of course, as the MvI is a tool ran on the system of the end-user.
It is the whole of MvK and MvS that should run as if it is running forever.

\section{\axiomScalability}
The Modelverse should be scalable in terms of computation, memory, number of users, number of models, and the size of individual models.
Related to the previous axiom, scalability should still be maintained even if the Modelverse is forever running.
Combined with scalability is performance: even if operations are scalable in terms of complexity, the total time taken by execution should also be as low as possible.

Due to our split in multiple components, we can also split up our scalability requirements over these components:
\begin{itemize}
\item The MvI needs to be scalable in performance, of course, though the size of models will be relatively small compared to those processed by the MvK or MvS, because the models being worked on will always be submodels of the \textit{complete} Modelverse model.
More important for the MvI is the scalability in the size of the model for visualization and presentation.
Depending on the domain, an implementation might provide further methods for abstraction of components.
\item The MvK needs to be scalable in performance, again, but mainly in the processing of action code constructs.
An MvK instance should be easily parallelizable up to the ``1 MvK per user'' threshold.
Beyond that limit, multiple MvKs would have to cooperatively work on a single block of action code, which is likely to hamper performance.
An MvK also needs to be scalable in the number of users it is able to handle.
\item The MvS needs to be scalable in performance, mainly in terms of the size of the complete Modelverse state.
It is non-trivial to distribute or parallelise, as operations are small and atomic, and all data needs to be shared between users.
The MvS should therefore be offloaded as much as possible, shifting all computation to the MvK.
This reduces the functionality of the MvS to that of a simple, but high-performance, data structure library.
Again, it should be scalable in the number of, possibly simultaneous, requests made, which differs from the total number of users.
\end{itemize}

\section{\axiomMinimalContent}
A minimal amount of content should be available in the Modelverse by default.
The content consists of the models necessary for bootstrapping, but also some default formalisms, such as \textsf{Petri Nets}, \textsf{Parallel DEVS}, \textsf{Statecharts}, \textsf{FTG+PM}~\cite{FTG+PM},~\ldots

For bootstrapping, the Modelverse contains a model of itself, which can then be compiled to a binary, executable outside of the Modelverse, or interpreted by the currently running MvK.
From this viewpoint, the Modelverse will be similar to Squeak~\cite{Squeak}, which is a Smalltalk interpreter written in Smalltalk.

Apart from formalisms, some models should also be present in the Modelverse.
These include the Formalism Transformation Graph (FTG), and the corresponding Process Model (PM), forming the FTG+PM.
The FTG model can be automatically constructed from the formalisms that are automatically detected in the Modelverse.
Combined with detecting the formalisms, it should also be possible to automatically detect all transformations defined between these formalisms, thus completing the FTG.
The PM model will be the driving force of the MvK and defines which operations to execute.
It can therefore be written in an action language, which defines the behaviour of the MvK, and thus the communication with the user.

\section{\axiomModelEverything}
Every element in the Modelverse needs to be explicitly modelled, using the most appropriate formalism.
This does not only include the typical elements, such as the models and metamodels, but should also go down to the level of the primitives such as Integer and Float.
This will allow for stronger model transformations, as they can transform (and access) literally everything.

Ultimately, a model of the Modelverse should also be present in the Modelverse, which closes the loop.
In the end, a compiled version needs to be used for pragmatic reasons, though this compiled version can be (automatically) compiled from the model that lives in the Modelverse.

Features like debugging, introspection, reflection, and self-modifiability will come from this axiom, as every part of execution is accessible for both reading and writing.

\section{\axiomHumanInteraction}
All interaction with the human user of the Modelverse needs to be explicitly modelled.
This includes timed behaviour of the Modelverse (\textit{e.g.}, time-out of requests), or even the complete communication protocol.
It is actually the MvI which will communicate with the Modelverse, though it will be guided by the user.

It should also be taken into account that the MvK will be (mainly) used by humans, and as such should be usable.
While most of this will be handled by the MvI, which provides the tool to the user, the fact that a human is behind all of it should be taken into account.
Possible applications for this are for performance evaluation: a human user has completely different (and likely slower) access patterns than an automated tool.
The predefined constructs and design of the system should also be usable by humans, specifically those that are non-experts in design of the Modelverse.
Enforcing strict metamodelling is part of the solution, as this offers users (and tools) a limited scope to worry about~\cite{StrictMetamodelling}.

\section{\axiomTestDriven}
Development on the Modelverse should happen using the model of the Modelverse, which can be simulated, and placed in a variety of circumstances which are hard to replicate in real-life situations.
A similar approach was taken by~\cite{DEVSinDEVS}, where a \textsf{DEVS} model was made of a distributed \textsf{DEVS} simulation kernel.
Modelling allowed them to replicate, among others, sudden disconnects, high latency connections, or different network topologies.
Furthermore, detailed, and perfectly deterministic, performance insights can be gained by the simulation of the model.
Certainly for parallel execution, this gives us deterministic thread interleavings, which can be crucial to debugging and performance analysis.

Functionality also needs to be checked as exhaustively as possible.
Certainly for the first axiom, critical bugs should be avoided as much as possible.
Because the Modelverse will have to communicate with a variety of tools, its interface will also have to be tested for conformance with the specifications.

\section{\axiomMultiView}
The Modelverse should support different views on the same model.
Examples include hiding parts of a model, or aggregating different elements into a composite element.
This gives rise to consistency management, as changes in one view will have to be propagated to all other views.

Multi-view should be handled at all components, as each component needs to allow it.
The MvI needs to provide operations to use the different views, the MvK needs to update the views and keep them consistent, and the MvS needs to provide these operations efficiently.
The MvS is least concerned with multi-view, as it sits at a lower level.

\section{\axiomMultiFormalism}
The Modelverse should support models which combine different formalisms.
Models should therefore be able to have a metamodel which is the combination of multiple (meta)models.
Inter-formalism links should also be possible, even if those cannot be typed within the respective formalism.
While the semantics of such a link depends on the domain, and therefore has to be provided by the user, the Modelverse should allow such links to be created and used.
Consequently, links between models should also be possible, which can then act as the type for those inter-formalism links.

Related, a single model should be able to have multiple metamodels.
A model could therefore be typed by a metamodel, but would also have to conform to a bigger metamodel, which contains the original metamodel as one of its elements.
This allows the reuse of models, even if the context surrounding the metamodel has changed.

\section{\axiomMultiAbstraction}
The Modelverse should support systems which are expressed using a set of models, all at a different level of abstraction.
Consistency management will again have to be handled here.

As was the case for multi-view, each component needs to think about multi-abstraction separately.
The exception is again the MvS, as it is at a lower level.
However, it can still (internally) use optimizations, knowing that some requests will be related to multi-abstraction.

\section{\axiomMultiUser}
The Modelverse should be able to serve multiple Modelverse Interfaces simultaneously.
A main concern to this is fairness between users: a user cannot wait for its turn infinitely long.
If a single user therefore uses all computational power, at the expense of other users, the code executed by this user will have to be automatically paused, marked as ``low priority'', or terminated.

User Access Control is related to this, as users should be able to configure the Read/Write/Execute status of their models.
As such, groups of users, with specific privileges, should also be supported.

If their access control allows it, users should also be able to read the state of the execution of other users.
This will allow for debugging with multiple users: user \textit{A} can execute code, with user \textit{B} being an automated debugging bot, which examines the state of user \textit{A}.

\section{\axiomInteroperability}
Different implementations of the Modelverse and its interface should be possible.
These implementations should all be able to communicate with each other, as long as they follow the same specification.
This is one of our main goals for specifying the interfaces between components.

Additionally, because the semantics of action code and its corresponding execution context is defined, different MvK's should be able to continue each other's execution, or interpret the execution context of other tools.
This can come in handy with different tools (\textit{e.g.}, a debugger, a compiler, or an interpreter) which might be developed independently, though are able to understand each other's information.

\section{Interconnections}
All of these axioms are related in some way, as the graph in Figure~\ref{fig:axioms_overview} shows.
We now continue by explaining the links between all concepts, using their label:
\begin{enumerate}
\item As the Modelverse will be forever running, there is a need for garbage collection or periodical maintenance to guarantee a decent performance.
\item Having everything explicitly modelled allows us to create a self-modifiable Modelverse, which helps us with the forever running axiom.
\item In the presence of multiple users, it is necessary to have the Modelverse running as a service, which implies that it should run forever.
\item Using the performance tests, combined with the MvK being modelled explicitly, it becomes possible to assess the scalability of the Modelverse algorithms under specific workloads.
\item Scalability is deeply connected with interoperability, as there is often a trade-off: increasing interoperability will decrease scalability and vice versa.
\item Having everything modelled explicitly requires the presence of at least a few basic formalisms. Ultimately, it also includes having a model of the Modelverse in the minimal content of the Modelverse.
\item By modelling everything, we will inevitably also have to model the interaction with the human.
\item The performance tests will use a performance model of the Modelverse, which is contained in the Modelverse. To that end, the Modelverse will simulate its own performance.
\item Multi-view requires the ability to model everything, as we will have to model all different views separately.
\item By modelling everything explicitly, we also need to model links between different formalisms, which is a requirement for multi-formalism models.
\item Interoperability between different Modelverse components becomes easier if each component is modelled explicitly, as it clearly defines the expected semantics.
\item Interoperability is an essential part of human interaction, as otherwise it would be impossible for both of them to communicate.
\item Multi-view and multi-formalism are related due to a view being possibly expressed in a different formalism.
\item Multi-view and multi-abstraction are related, as different views might be at different levels of abstraction.
\end{enumerate}

\begin{figure}
    \center
    \includegraphics[width=0.8\textwidth]{images/axioms_overview.eps}
    \caption{Overview of relations between all axioms}
    \label{fig:axioms_overview}
\end{figure}