search

openETCS / toolchain

WP7: Top Level Project for the toolchain
26 stars 30 forks source link

Need to get Safety properties and invariants to prove from WP2 #31

Closed stanpinteTheSignallingCompany closed 11 years ago

stanpinteTheSignallingCompany commented 11 years ago

During Track 1: model proving brainstorming session, it is obvious that the OpenETCS project is missing a list of Safety properties/invariants to prove. Some participants cite the famous example of safety invariant "two trains cannot be at the same place at the same time", but the only Subset-026 safety invariant that comes during the meeting is about braking curves: the speed of the train should always be below the max permitted speed.

Action: Email WP2 list and ask for such output, check with michael jastram WP3a leader as this should be included in WP3 backlog Status: TODO

sbaro commented 11 years ago

As for the allocation of these requirements toward WP2, I am not sure it really belongs here. As far as I understand, WP2 provides requirements on the tools, model, methods, and so on. These requirements are at the "meta" level. What is discussed here is to provide requirement as roots of the safety proofs. It should then belong to the same WP as other safety issues, because it is a part of the safety case. What is required (IMHO) from WP2 on this topic should be to provide requirements on what should be proved, and how it should be proved.

stanpinteTheSignallingCompany commented 11 years ago

Dear Sylvain,

I agree with you that it would be a good start if WP2 can provide requirements on what should be proved, and how it should be proved.

Is this already in the WP2 Dow?

Very kind regards

Stan

sbaro commented 11 years ago

Dear Stanislas,

First, I wish you a happy new year!

Yes, IMHO, WP2's role is to stay at "meta level". The purpose is to define:

Best regards, Sylvain.

armandnachef commented 11 years ago

Hello,

I agree about the WP2's role. However safety properties and invariants should be defined somewhere. We need to have an idea about such properties in order to define and select the adequate tools in WP7. It makes sense to define them in both WP3 and WP4.

I found some safety properties of the system in a thesis on internet: "http://prr.hec.gov.pk/Chapters/1060S-4.pdf" For these safety properties, defining them using a first-order logic language could be very useful.

At CEA we have developed:

I would suggest considering these 2 languages that are supported by tools for proofs

Best regards Armand

sbaro commented 11 years ago

Hello Armand,

Sorry for this late answer!

In the CENELEC compliance process, one of the first document of the safety case is the Preliminary Hazard Analysis document, which gives the higher level properties for the system. It will contain head-to-head collision, derailment, electrocution... and depends most on the responsibilities of the system than on its functionalities.

The safety analyses should then refine and allocate these properties into the system functions. For example, if I have a "Train tracking" function, the property should ensure that my trains are properly tracked (which will in turn climb back to the top properties on the collisions and derailment).

ERTMS provides a set of higher level safety properties in the SUBSET 91. I think it could be used as a start for the safety analysis, even if we do not have the guarantee that these properties are sufficient to ensure safety. They are lower level to what should be the PHA, so it should be easier to use this set than to produce one ourselves.

You will find subset 91 here : http://www.era.europa.eu/Document-Register/Pages/UNISIGSUBSET-091.aspx

The PhD document you sent is interesting for its formalization, but not really convincing for its properties. In particular for a switch, the derailment will generally be due to an overspeed on the deviated branch, or to the fact that the train enter the switch when the point is not locked or locked in improper position (but I am not an expert on these topics).

Best regards, Sylvain.

GuillaumePottier commented 11 years ago

New release of WP2 D2.5 Methods and tools benchmarking methodology defines safety properties to prove for the benchmark.

MariellePetitDoche commented 11 years ago

SSHA has been included in the Safety process to define the safety properties to prove.