search

openETCS / model-evaluation

part of WP7: collects the various activities regarding selecting a tool and formal specification for modeling
13 stars 20 forks source link

ERTMSFormalSpecs assessment by Assessor 2 / semi-formal model / timeouts and truth tables #43

Closed stanpinteTheSignallingCompany closed 10 years ago

stanpinteTheSignallingCompany commented 11 years ago

There is the following note:

"The current model does not cover the § 3.5 on session management and the §4, thus it is di cult to evaluate the capabilities of the language to treat time-outs and truth tables."

This statement is incorrect, as a good deal of §3.5 is implemented, including timeouts (see for instance this screenshot for timeouts).

timeout_screenshot

Also, the high-priority elements that should be modelled to prove the support of truth tables (HIGH PRIORITY §4.6.2 (Transitions Table) and §4.6.3 (Transitions Condition table)) have been 100% and successfully modelled.

Therefore, could you please:

MariellePetitDoche commented 11 years ago

In the version of the model evaluated, §3.5 is partialy implemented :

session_management

concerning true table, condition with high priority are not implemented (at least conditions 1, 5, 6, 10, 50) :

truetable

however, this is not a problem due to that other models of the benchmark cover only in part the high priority items, but it does not allow me to assess these criteria.

Svitlana-Lukicheva commented 11 years ago

It is true that the Section 3.5 is not fully implemented, but it has enough implementation to show that timeouts are supported (see Stan's screenshot).

The priorities between the conditions of the Table 4.6.2 are fully implemented by the procedure Kernel.ModeTransitions.UpdateMode. The conditions themselves are implemented by the corresponding functions of the namespace Kernel.ModeTransitions. Only the conditions in blue on your screenshot are not implemented, so the conditions 1, 5, 6, 10 and 50 are implemented.