Means of description and methodology criteria (Template)
What is the main usage of this methodology ? At which step of a classical process it is used ?
Especially how where step of the proposed process it can cover (see D2.3) :
- system specification
- subsystem specification
- software requirements and specifications
- software architecture and design
- code development
- test generation
- validation
- model verification
- code verification
- safety and fault anaysis
- other (give details)
Which criteria for software requirement specification are covered by the methodology (see EN50128 table A.2) :
- formal methods
- modeling
- structured methodology
- decision table
Which criteria for software architecture are covered by the methodology (see EN50128 table A.3) :
- defensive approach
- fault detection & diagnostic
- error detecting code
- failure assertion programming
- diverse programming
- memorising executed cases
- software error effect analysis
- Information Encapsulation
- fully defined interface
- formal methods
- modelling (supported by computed aided design and specification tools or not)
- structured methodology
- others (give details)
Which criteria for software design and implementation are covered by the methodology (see EN50128 table A.4) :
- formal methods
- modeling
- modular approach (mandatory for Sw design and implementation)
- components
- design and coding standards (mandatory for Sw design and implementation)
- strongly typed programming language
- others (give details)
: {{TODO | Do we need to detail code criteria ?}}
: {{TODO | Do we need to detail criteria for VnV and test ?}}
What is the degree of formality (see D.2.1 §1) ?
- informal (incomplete set of symbols, logical syntax and semantics are not defined)
- semi-formal (set of symbols completly defined, logical syntax partially defined, semantics not defined)
- formal (set of symbols, syntax and semantics are mathematically defined to be unambiguous, complete and consistent)
What kind of representation (see D.2.1 §3) ?
- textual
- mathematical symbols or code
- graphical
How can safety properties be provided in a declarative, simple and formal language (R-WP2/D2.3.0-X-25) ?
Shall the formal methodology formalize (R-WP2/D2.3.0-X-27):
- State machines,
- Time-outs,
- Truth tables,
- Arithmetics,
- Braking curves,
- Logical statements.
What are the capabilities of the methodology to capture the structure of a system (D.2.1 §2.1) ?
What are the capabilities of the methodology to capture the behaviour of a system (D.2.1 §2.1) ?
Does the methodology provide an explicit time representation (D.2.1 §2.1) ?
What are the pro/cons of the methodology to cover the following requirement ?
-
R-WP2/D2.3.0-X-24 The model formalism shall be easily understandable by the domain experts.
-
R-WP2/D2.3.0-X-26 The formal model shall be understandable by or exportable to many tools (SCADE, Simulink, B tools, OpenETCS tool chain. . .) ?
Does the methodology support formal proof (D2.1 § 2.1) ?
Does the methodology cover the following requirements ?
-
R-WP2/D2.3.0-X-29 It shall be possible to assert logical properties on the model (i.e., invariants).
- R-WP2/D2.3.0-X-29.1 It shall be able to check the conformance of these properties at runtime.
- R-WP2/D2.3.0-X-29.2 It shall be able to prove the conformance of the model to these properties.
Does the methodology provide an executable formal model (D2.3.0-X-28) ? Does the methodology allow step-by-step debugging mode with reports on states, variables and I/O changes ? Does the methodology provide access to high level construction of the inputs ?
How dows the methodology manage traceability of the requirements ?
How is the methodology documented ?
How can feedback be found on the methodology ?
give details.