Many research works had the aim of creating frameworks able to model systems, of de ning their requirements and properties, and of verifying their satis ability. Many approaches involve the usage of the Model Driven Engineering throughout the whole system lifecycle in order to build systems that are correct by construction. Using models as primary artefacts helps to reduce costs and time of development. The possibility of having automatic code generation from model tools enact the possibility to produce (theoretically) bug-free code starting from correct models. In this work we describe the usage of a modelling and veri cation tool, MetaMORP(h)OSY, for performing quality control in E-Health Domain.
In many applications, standards and/or regulatory processes are de ned to ensure that systems are going to operate as intended. In critical systems this is very important, because an error or a failure could lead to serious damages in terms of human lives, environment and money. In these systems it is necessary to use formal methods, i.e. mathematical techniques used for the speci cation, development and veri cation of software and hardware systems.
In recent years, Model Driven Engineering (MDE) has developed a lot, laying its foundations on the massive use of models as its primary artefacts.
In literature, many research works have been devoted to exploit the abstraction resulting from the creation of models in the MDE and in the application of Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). This volume is published and copyrighted by its editors. SEBD 2020, June 21-24, 2020, Villasimius, Italy. the modelling techniques on various kinds of systems. In particular, researchers are trying to create frameworks that allow to completely describe systems (and their requirements and properties) and to verify their correctness.
The principle is to use MDE approaches throughout the system lifecycle. The aim is to build systems that are correct by construction. Using models as primary artefacts helps to reduce costs and time of development, and since automatic code generation from model tools are already available, it is clear that is possible to produce (theoretically) bug-free code (starting from correct models). The standard use of the MDE involves the use of a Domain Speci c Modelling Language (DSML) for the de nition of system models. With this language, di erent levels of abstraction of the system under study are created. These abstraction levels must somehow contain consistent in formation about the system.
This is the reason why Model-to-Model (M2M) and Model-to-Test (M2T) translation tools are used as bridges between abstraction levels.
These transformations, besides being useful to treat models in the most convenient way, allow us to introduce automation in our process. In order to build a process that leads automatically (or semi-automatically) to the creation of a correct system, it is necessary to solve some problems of high complexity, for example: { to guide the user in the construction of an high-level model of the system and its speci c analysis properties; { automating the de nition and con guration of the analysis process (e.g. by calling the right tools at the right time)
Such approach can be used also to setup, in a very fast and exible way,
many di erent kind of systems, that can be applied to the analysis of complex
domains, like social networks [1{4], big-data, or human-understanding interfaces
[
Many works [
MetaMORP(h)OSy exploits a multi-agent modelling paradigm. A meta-formalism extending UML is used to express actors, system components and requirements. Algorithms are used in the design phase to translate Multi Agent Systems models into appropriate formal models.
MetaMORP(h)OSy implements a methodology for the design, validation and veri cation of critical systems. For this purpose, it uses techniques and approaches of MDE and MAS. In particular, MetaMORP(h)OSy exploits a multiagent modelling paradigm. A meta-formalism extending UML is used to express actors, system components and requirements. Algorithms are used in the design phase to translate MAS models into appropriate formal models. The de nition of requirements allows the choice of appropriate Observers to be performed for model analysis. After the validation of the design models, vertical transformations are implemented, which produce stubs for the generation of the system at run-time. The framework must generate monitors during the design and execution phase in order to allow the veri cation of the requirements. In particular, the monitors in the execution phase must compare the behavior of a system under analysis with the one predicted in design analysis. 2.2
METAMORP(h)OSy provides the same graphic language for the system specication and its requirements formulation. This language is formally de ned by a meta-model. The MetaMORP(h)OSy pro le must allow the de nition of: { structural and behavioural views of the system; { system properties and requirements to be veri ed; { methods, techniques and metrics for analysing or measuring properties and requirements; { expected and measured workloads of the systems.
Being MetaMORP(h)OSy designed to be used for critical systems, it
allows the speci cation of temporal behaviour of agents and real-time
properties[
Agents are characterized by their beliefs, the objectives they want to achieve and the plans available to achieve them. RT-AML pro le uses four diagrams for MAS behaviours description: Class diagrams, RT Agent Diagrams, RT-Activity diagrams and RT-Sequence diagrams. Class diagrams are the same of UML class diagrams. They are used when it is not useful to describe objects as agents (for example in case of passive entities). The RT-Agent diagrams are the core of the RT-AML pro le. They describe agents' structures, goals and beliefs. In addition, they declare the actions and the plans they can execute.
The RT-Activity diagrams allow for description of agents plans. The
RTSequence diagrams describe agents' collaborations (and/or competitions). Their
main goal is to de ne exchanges of messages and events (real-time stimula)
during execution of agents plans. As seen in Amato and Moscato 2015[
The AgentRT stereotype de nes the structure of agents. The PlanRT stereotype de nes the plans, which in turn de ne the behaviour of agents. Plans are associated with objectives, and typically these are common to multiple agents, who will work together to achieve them.
The DgoalRT stereotype de nes decidable targets for AgentRTs, where a decidable target is a target whose reachability can be achieved under real-time constraints. The BeliefRT stereotype is used to model what the agent knows, in terms of internal status, the information about other agents and the external environment.
Stereotypes needed to model agent plans are de ned in the RT-Activity diagram pro le. RT-Activity Diagram inherits all these elements from the UML Activity Diagram, rede ning states and transitions to specify real-time constraints. There are six stereotypes created ad-hoc:
ActionStateRT, InitialState, FinalState, TransitionRT, SendObjectRT and ReceiveObjectRT. When an agent starts a plan, he has information about his surroundings.
These Beliefs usually make up the initial state of the activity diagram, and they are speci ed as properties of the Initial State Stereotype. FinalState refers to a DGoalRT, and it is the nal state of the activity diagram. Usually the temporal properties are relative to the nal state. ActionStateRT derives from the classic state of the Activity Diagram UML. It is basically a state subject to real-time constraints. The stereotype in fact includes properties such as ExecActionTime, that is the time it takes to execute the action. In particular, to describe situations in which an agent sends or receives objects (messages or events), the stereotypes SendObjectRT and ReceiveObjectRT have been introduced. The last stereotype introduced for Activity Diagrams is TransitionRT, which is used to de ne time constraints on state transitions. 2.3
Main elements of the RT-Sequence Diagram are StimulusRT and MultiStimulusRT. Before introducing the stereotype StimulusRT we recall the fact that a sequence diagram is basically composed by objects and lifelines. In this context, stimuli are messages that objects can send to themselves. There are ve types of stimuli: Call, Send, Return, Create and Destroy. StimulusRT is used, therefore, to de ne stimuli subject to real-time constraints. Each StimulusRT element has the following properties: { StartTime: when the decision to send a message during the pian is made. { SendTime : when the message is sent. { TransmissionTime : the time required to transmit the message. { StartReceiveTime : the time the receiver starts receiving the message. { EndReceiveTime: the time when the receiver has nished receiving the message. { Deadline : the deadline for broadcasting. { MessageSync: used to specify whether the message is synchronous or not.
MultiStimulusRT is derived from the StimulusRT stereotype, and it is used to de ne redundancy in message reception. MetaMORP(h)OSy has separate pro les for de ning requirements and properties of systems. This allows to demand di erent requirements on the same system at di erent times, which is why requirement and property speci cations are de ned outs ide of the agent stereotypes.
A requirement is a list of properties that Observers will analyse on the models (at design-time or run-time). The properties can be functional or non-functional.
MetaMORP(h)OSy basic pro le for properties de nes stereo types for properties such as Availability, Reliability, Schedulability, Performances, etc. Obviously, if the properties are non-functional, it is necessary to de ne metrics for their de nition, evaluation and monitoring. Users can add other metrics and properties to the basic MetaMORP(h)OSy pro le.
Proper modules called Obervers (whose structure is de ned in the modelling pro le too) choose the best suitable Translator in the framework to execute proper Model Transformations and to verify requirements.
Since MetaMORP(h)OSy covers all system life cycle, it uses particular Observers at run-time for monitoring and testing purposes. So, Observers are divided by the pro le into: Design Time Observers and Run Time Observers. They can be further specialized depending on translation algorithm, and analysis methods are used to analyse properties and requirements on system components.
Observers can be associated to Structural and behavioural components and obviously to the property to analyse or to monitor, as well as to the metrics used to collect and to produce results. The Observers introduce the intelligence needed to automate the system analysis. They are generated from the analysis models and they are dependent on the kind of the analysis that must be performed.
The Observers are in charge of automatically establishing and realizing the speci c MDE approach to validation and veri cation of the system under study. They use the UML models of the system and the information contained in the analysis models in order to choose a suitable analysis process and generate the formal models needed to ful l the analysis objectives. They enact the process, also invoking the proper analysis/solution tools. The overall MetaMORP(h)OSy component architecture is depicted in gure 2. 3
This section describes the specialization of MetaMORP(h)OSy methodology
applied in processing data[
These new Agents specialize the AgentRT stereotype are: { Patient represents the entity that possess Electronic Health Record and grant the authorizations for the access to records by other agents; { DataController: users can use this stereotype in order to declare agents like Hospitals that implement the E-Health system ; { DataProcessor stereotype de nes providers for records management and storing; { DataSubProcessor usually refers to Cloud Storage providers; { Physician is the entity related to doctors that interacts with patients. In particular, Family doctors and doctors who are eventually involved in emergencies specialize this stereotype.
The BeliefRT is specialized introducing: { HealthRecord: the electronic health record of the patient; { EnCryptedHR: encrypted version of the health record; { HiddenRecord: used for hiding the health record to any agent able to read the patient's data; { EncryptKey: used to encrypt data; { DecryptKey: used to decrypt data; { AccessAuth: physicians authorizations;
Please note that access to encrypted data is achieved through the coupled use
of encryption and decryption keys. In Amato and Moscato 2015[
The goal is to obtain the following behavior: if an agent executes a plan, whose goal is reachable. In case of access of a patient's record without having any valid authorization, the veri cation must fail.
In Amato and Moscato 2015[
The problem is the storage of the health record on a third-party storage server (DataProvider in the following).
The generic owner of the record is a patient (thePatient in the following). ThePatient can always read its Health Record (HR). In order to store the record on the storage service provider, a previous encryption of the record has to be done.
The encryption is executed directly on the patient's smart device. The doctor (theDoctor) can access the record only if it is authorized by thePatient. By the way, the doctor cannot own the description key of thePatient. For this reason, during the authorization process, theDoctor shares its encryption key with the Patient, so that it can encrypt the HR using this key.
In order to manage emergencies, thePatient stores on the DataProvider another encrypted version of its HR. This time, in the encryption process, a common key is used.
DataProvider, thePatient and theDoctor have been de ned as agents, so they must be described in a structural view with appropriate Agent Diagrams. A BeliefDesire-Intention logic approach has been used in de ning Agent Diagrams.
Its beliefs contain information about thePatient's, theDoctor's and emergency keys. In this diagram only three plans have been considered: { Save: for saving the record on DataProvider; { ReadRecord: to read the record from DataProvider; { Authorize: to grant authorization to doctors to retrieve encrypted records from DataProvider.
Each Plan is associated to a Goal. It is reached when the nal action of the plan is executed. It is important to notice that beliefs with the same name share the same information between agents.
For each agent plan, the user must de ne an activity diagram. In the following it will be reported activity diagrams of Save and Authorize plans. Please recall the fact that plans are used to reach a goal, and very often this is obtained thanks to the communication between agents. This concept brings the notion of synchronization, expressed in the activity diagrams through guards on control ow edges. Guards contain declarations of events that are asserted or waited during plans executions.
The activity diagram we are going to analyse is the Save plan diagram, depicted in Figure 3. The objects on the left side of an activity diagram correspond to the diagram inputs, while the objects on the right side correspond to the diagram outputs. Please notice that in the Save plan there are three parallel requests for saving the record encrypted using: its encryption key, its common encryption key for emergencies and its authorized doctor's encryption key.
The second activity diagram, depicted in Figure 4, describes the Read plan.
It shows actions that are executed by theDoctor when it requests a normal authorization to read the health record. Please notice that in this diagram there are two nal states: one linked to the failure of the plan (ErrorAuth?) and one linked to the success of the plan (after receiving OkAuth!, it starts the decryption, and then theDoctor can access the record).
To nish the behavioral description of the system, proper sequence diagrams must be provided, in these diagrams, asserted events, which appear in agents' activity diagrams, are declared.
At the end of structural and behavioral description of the system, the user must prepare an Observer Diagram to declare the type of the analyses and monitoring activities it want to perform on the system.
MetaMORP(h)OSy o ers many Observers which are already implemented.
In some cases, it could be useful to de ne an ad-hoc Observer algorithm, such
as it was done in Amato and Moscato 2015[
A timed automaton is a nite state machine extended with a nite set of real-valued clocks. During a run of a timed automaton, clock values increase all with the same speed. Along the transitions of the automaton, clock values can be compared to integers. These comparisons are used in order to evaluate automaton transitions.
Without deepening into details, the Observer algorithm translates the RTAML models D into a Timed Automata. This allows the use of Timed Automata analysis tools for verifying requirements. The last thing that has to be done is the translation of the data privacy requirement in an analyzable property for a Timed Automata Model Checker.
In Amato and Moscato 2015[
In this work we have shown that the adoption of Multi-Agent System models, combined with the use of Model-Driven Engineering can provide signi cant advantages. The combination of MAS and MDE leads exibility and intelligence in the analysis of properties and requirements of systems.
Frameworks like MetaMORP(h)OSy helps us in automating (or semi-automating) the veri cation and validation process. When adopting this framework, the user only needs to derive his particular modelling pro le from the standard Meta MORP(h)OSy's RT-AML meta-model. As a further step, the user must produce proper diagrams and observers, in order to analyse system properties and requirements in the correct way.
In the last part of the work, an architectural description of MetaMORP(h)OSy is provided, with speci c focus on its RT-AML pro le specialization for particular purposes. It has been described, in addition, an example of MetaMORP(h)OSy application in E-Health domain.
Through this work, the advantages of using MetaMORP(h)OSy, in system property analysis have been highlighted for e-Health domain. We rmly believe that this kind of applications will be adopted and developed not only in the academic world, but certainly in industry world, too.
This work was funded by \Synergy-net: Research and Digital Solutions against Cancer" Project (funded in the framework of the POR Campania FESR 20142020).