Le 2 juin 2011 à 04:10, Topcased user list where issues are discussed a écrit :

> Hi, My name is Nayun Cho, graduate student at Konkuk Univ. in South Korea.
> 
> 

Hi Nayun Cho,

> 
> Nowadays, I’m using Topcased for drawing UML diagrams in Eclipse.
> 
> Thus, I found great features of Topcased, especially Model simulation.
> 
> I think that “Model simulation” is kind of “Model checking” technique which 
> validates system or software whether it fulfills its requirements or not.
> 
> Q1. Is it correct or not?

Yes and no.

Model checking is a specific technologies that aims at provide a complete 
exhaustive verification that the model fulfills its requirements. In order to 
be complete, it requires that the model exhibits a finite behavior or that its 
behavior can be automatically  be abstracted to a model that has a finite 
behavior. Another problem is that this behavior should not be to complex in 
order to be able to represent the finite abstraction with the current hardware 
(usually, a very big amount of memory is required).

The end user need to provide a formal specification of its requirements that is 
used by the model checker to analyze the model behavior and check that it 
satisfy them.

Model checking is an automated technology that answers yes if the behavior 
satisfies its requirements and provide a counter example that is does not if it 
is the case. Then the user can analyze the counter example to understand why 
the model does not satisfy the requirements.

In order to analyze the counter example, the user can rely on a model animator 
which is a graphical interface that allows to show the various execution steps 
and the evolution of the model behavior related data.

Model simulation is another behavioral verification technology that does not 
aim at being complete. It is mainly targeting model validation. The end user 
can execute the model to check that its behavior is indeed the one he had in 
mind when he designed it.

In order to visualize the result of the execution, the user can use the same 
model animator he can also use to understand the counter example provided by 
the model checker.

The simulation can be offline using a scenario providing all the inputs needed 
to execution the model, or online, then the simulator asks the user for the 
inputs when they are needed.

> 
> 
> 
> Moreover, I think that it can employ only for “interaction diagram (such as 
> activity, sequence diagram)”.

Yes, it is mainly related to behavior diagrams as the model must be executed.

> 
> Q2. Can we use that kind of validation into “structural diagram (such as 
> class, component diagram)”??
> 
> ( This means when we want to validate the architecture of system or software 
> whether it is suitable or not )
> 

You need to be able to define what is a valid architecture. If you are able to 
express it formally. For example, using OCL constraints at the metamodel level, 
then you can do some kind of very simple model verification.

> 
> 
> Q3. Furthermore, if Q2’s answer contains “only for interaction diagram”, the 
> architecture of system or software should transform into “interaction 
> diagram” for use “Model Simulation” ?
> 

In order to translate your structural diagram in a behavior diagram, you need 
to define what is the behavior of a structural diagram... For example, the 
behavior of a class and object diagram is a scenario that builds the objects 
out of the class...

But, usually, there is no behavior inside the structural diagrams...

> 
> 
> Q4. Also, is there any functionality which processes model-transformation 
> between “structural diagram” into “interaction diagram” for use “Model 
> Simulation” ??
> 

You need to be more precise. The only one I know is the previous example that 
is needed to initialize State diagrams from object diagrams with State machine 
associated to classes.

Best regards,
Marc

> 
> 
> If you give answers, that would be great help to using Topcased.
> 
> Thank you
> 
> 
> 
> Best Regards,
> 
> 
> 
> 
> 
> _______________________________________________
> Topcased-users mailing list
> [email protected]
> http://lists.gforge.enseeiht.fr/cgi-bin/mailman/listinfo/topcased-users

Marc Pantel
Maître de Conférences en Informatique
Assistant Professor in Computer Science
IRIT - Institut de Recherche en Informatique de Toulouse - CNRS
N7 - INPT - Université de Toulouse - France - Europe
phone +(33) 534 32 2185
fax +(33) 534 32 2157
cell +(33) 676 221 687





_______________________________________________
Topcased-users mailing list
[email protected]
http://lists.gforge.enseeiht.fr/cgi-bin/mailman/listinfo/topcased-users

Reply via email to