Tool Development Roadmap - Revision history

imported>Tommy at 09:50, 12 September 2013

2013-09-12T09:50:44Z

← Older revision		Revision as of 09:50, 12 September 2013
Line 11:		Line 11:
	!Status		!Status
	\|-		\|-
	\|rowspan="4"\|'''Platform maintenance'''<br/>[Systerel / ~~Dusseldorf~~]		\|rowspan="4"\|'''Platform maintenance'''<br/>[Systerel / Düsseldorf]
	\|3.2.1		\|3.2.1
	\|D3.2, D3.3, D3.4		\|D3.2, D3.3, D3.4
Line 32:		Line 32:
	\|		\|
	\|-		\|-
	\|rowspan="9"\|'''Automated Proof and Model-checking'''<br/>[Systerel / ~~Dusseldorf~~ / Southampton]		\|rowspan="9"\|'''Automated Proof and Model-checking'''<br/>[Systerel / Düsseldorf / Southampton]
	\|3.3.1.a		\|3.3.1.a
	\|D3.2, D3.3		\|D3.2, D3.3
Line 78:		Line 78:
	\|		\|
	\|-		\|-
	\|rowspan="9"\|'''Language extension'''<br/>[Southampton / Systerel / ~~Dusseldorf~~ / All Partners]		\|rowspan="9"\|'''Language extension'''<br/>[Southampton / Systerel / Düsseldorf / All Partners]
	\|3.4.1.a		\|3.4.1.a
	\|D3.3		\|D3.3
Line 124:		Line 124:
	\|		\|
	\|-		\|-
	\|rowspan="5"\|'''Composition and decomposition'''<br/>[Southampton / ~~Dusseldorf~~ / Systerel]		\|rowspan="5"\|'''Composition and decomposition'''<br/>[Southampton / Düsseldorf / Systerel]
	\|3.5.1.a		\|3.5.1.a
	\|D3.2		\|D3.2
Line 151:		Line 151:
	\|		\|
	\|-		\|-
	\|rowspan="6"\|'''Multi-simulation framework development'''<br/>[Southampton / ~~Dusseldorf~~]		\|rowspan="6"\|'''Multi-simulation framework development'''<br/>[Southampton / Düsseldorf]
	\|4.2.1.a		\|4.2.1.a
	\|D4.2		\|D4.2
Line 182:		Line 182:
	\|		\|
	\|-		\|-
	\|rowspan="5"\|'''Model simulation with ProB'''<br/>[~~Dusseldorf~~]		\|rowspan="5"\|'''Model simulation with ProB'''<br/>[Düsseldorf]
	\|4.3.1.a		\|4.3.1.a
	\|D4.2		\|D4.2
Line 208:		Line 208:
	\|		\|
	\|-		\|-
	\|rowspan="4"\|'''Model-based testing'''<br/>[~~Dusseldorf~~ / Southampton]		\|rowspan="4"\|'''Model-based testing'''<br/>[Düsseldorf / Southampton]
	\|4.4.1.a		\|4.4.1.a
	\|D4.3		\|D4.3
Line 229:		Line 229:
	\|		\|
	\|-		\|-
	\|rowspan="4"\|'''Code generation'''<br/>[Southampton / ~~Dusseldorf~~]		\|rowspan="4"\|'''Code generation'''<br/>[Southampton / Düsseldorf]
	\|4.5.1.a		\|4.5.1.a
	\|D4.2		\|D4.2

imported>Nicolas: /* Task Status */

2013-09-10T15:45:42Z

Task Status

← Older revision		Revision as of 15:45, 10 September 2013
Line 124:		Line 124:
	\|		\|
	\|-		\|-
	\|rowspan="5"\|Composition and decomposition		\|rowspan="5"\|'''Composition and decomposition'''<br/>[Southampton / Dusseldorf / Systerel]
	\|3.5.1.a		\|3.5.1.a
	\|D3.2		\|D3.2
Line 151:		Line 151:
	\|		\|
	\|-		\|-
	\|rowspan="6"\|Multi-simulation framework development		\|rowspan="6"\|'''Multi-simulation framework development'''<br/>[Southampton / Dusseldorf]
	\|4.2.1.a		\|4.2.1.a
	\|D4.2		\|D4.2
Line 182:		Line 182:
	\|		\|
	\|-		\|-
	\|rowspan="5"\|Model simulation with ProB		\|rowspan="5"\|'''Model simulation with ProB'''<br/>[Dusseldorf]
	\|4.3.1.a		\|4.3.1.a
	\|D4.2		\|D4.2
Line 208:		Line 208:
	\|		\|
	\|-		\|-
	\|rowspan="4"\|Model-based testing		\|rowspan="4"\|'''Model-based testing'''<br/>[Dusseldorf / Southampton]
	\|4.4.1.a		\|4.4.1.a
	\|D4.3		\|D4.3
Line 229:		Line 229:
	\|		\|
	\|-		\|-
	\|rowspan="4"\|Code generation		\|rowspan="4"\|'''Code generation'''<br/>[Southampton / Dusseldorf]
	\|4.5.1.a		\|4.5.1.a
	\|D4.2		\|D4.2

imported>Nicolas: /* Task Status */

2013-09-10T15:37:51Z

Task Status

← Older revision		Revision as of 15:37, 10 September 2013
Line 11:		Line 11:
	!Status		!Status
	\|-		\|-
	\|rowspan="4"\|Platform maintenance		\|rowspan="4"\|'''Platform maintenance'''<br/>[Systerel / Dusseldorf]
	\|3.2.1		\|3.2.1
	\|D3.2, D3.3, D3.4		\|D3.2, D3.3, D3.4
Line 32:		Line 32:
	\|		\|
	\|-		\|-
	\|rowspan="9"\|Automated Proof and Model-checking		\|rowspan="9"\|'''Automated Proof and Model-checking'''<br/>[Systerel / Dusseldorf / Southampton]
	\|3.3.1.a		\|3.3.1.a
	\|D3.2, D3.3		\|D3.2, D3.3
Line 78:		Line 78:
	\|		\|
	\|-		\|-
	\|rowspan="9"\|Language extension		\|rowspan="9"\|'''Language extension'''<br/>[Southampton / Systerel / Dusseldorf / All Partners]
	\|3.4.1.a		\|3.4.1.a
	\|D3.3		\|D3.3

imported>Nicolas: /* Task Status */

2013-09-10T15:31:24Z

Task Status

← Older revision		Revision as of 15:31, 10 September 2013
Line 36:		Line 36:
	\|D3.2, D3.3		\|D3.2, D3.3
	\|Enrich SMT support for Event-B mathematical language		\|Enrich SMT support for Event-B mathematical language
	\|		\|Done, covered in D3.3.
	\|-		\|-
	\|3.3.1.b		\|3.3.1.b
	\|D3.2, D3.3		\|D3.2, D3.3
	\|Assess SMT solvers effectiveness		\|Assess SMT solvers effectiveness
	\|		\|Done, covered in D3.3.
	\|-		\|-
	\|3.3.2.a		\|3.3.2.a
	\|D3.2		\|D3.2
	\|Develop specialised prover tactics for case studies		\|Develop specialised prover tactics for case studies
	\|		\|Not done yet, expecting feedback from case studies
	\|-		\|-
	\|3.3.2.b		\|3.3.2.b
	\|D3.2		\|D3.2
	\|Add FAQ in handbook with tips on prover tactics		\|Add FAQ in handbook with tips on prover tactics
	\|		\|Partially done, paragraph exists: [http://handbook.event-b.org/current/html/use_provers_effectively.html], to be enriched
	\|-		\|-
	\|3.3.3.a		\|3.3.3.a

imported>Nicolas: /* Task Status */

2013-09-10T15:05:34Z

Task Status

← Older revision		Revision as of 15:05, 10 September 2013
Line 15:		Line 15:
	\|D3.2, D3.3, D3.4		\|D3.2, D3.3, D3.4
	\|Answer questions from ADVANCE partners		\|Answer questions from ADVANCE partners
	\|Done, covered.		\|Done, covered in D3.3.
	\|-		\|-
	\|3.2.2		\|3.2.2
	\|D3.2, D3.3, D3.4		\|D3.2, D3.3, D3.4
	\|Process feature requests and platform issues		\|Process feature requests and platform issues
	\|Done, covered.		\|Done, covered in D3.3.
	\|-		\|-
	\|3.2.3		\|3.2.3
	\|D3.2, D3.3, D3.4		\|D3.2, D3.3, D3.4
	\|Maintain and evolve model editors		\|Maintain and evolve model editors
	\|Done, covered		\|Done, covered in D3.3.
	\|-		\|-
	\|3.2.4		\|3.2.4

imported>Nicolas: /* Task Status */

2013-09-10T15:03:40Z

Task Status

← Older revision		Revision as of 15:03, 10 September 2013
Line 15:		Line 15:
	\|D3.2, D3.3, D3.4		\|D3.2, D3.3, D3.4
	\|Answer questions from ADVANCE partners		\|Answer questions from ADVANCE partners
	\|		\|Done, covered.
	\|-		\|-
	\|3.2.2		\|3.2.2
	\|D3.2, D3.3, D3.4		\|D3.2, D3.3, D3.4
	\|Process feature requests and platform issues		\|Process feature requests and platform issues
	\|		\|Done, covered.
	\|-		\|-
	\|3.2.3		\|3.2.3
	\|D3.2, D3.3, D3.4		\|D3.2, D3.3, D3.4
	\|Maintain and evolve model editors		\|Maintain and evolve model editors
	\|		\|Done, covered
	\|-		\|-
	\|3.2.4		\|3.2.4

imported>Nicolas: /* Task Status */

2013-09-09T13:53:36Z

Task Status

← Older revision		Revision as of 13:53, 9 September 2013
Line 5:		Line 5:

	{\| border="1"		{\| border="1"
			!Task
	!Task Id		!Task Id
	!Deliverable		!Deliverable
Line 10:		Line 11:
	!Status		!Status
	\|-		\|-
			\|rowspan="4"\|Platform maintenance
	\|3.2.1		\|3.2.1
	\|D3.2, D3.3, D3.4		\|D3.2, D3.3, D3.4
Line 30:		Line 32:
	\|		\|
	\|-		\|-
			\|rowspan="9"\|Automated Proof and Model-checking
	\|3.3.1.a		\|3.3.1.a
	\|D3.2, D3.3		\|D3.2, D3.3
Line 75:		Line 78:
	\|		\|
	\|-		\|-
			\|rowspan="9"\|Language extension
	\|3.4.1.a		\|3.4.1.a
	\|D3.3		\|D3.3
Line 120:		Line 124:
	\|		\|
	\|-		\|-
			\|rowspan="5"\|Composition and decomposition
	\|3.5.1.a		\|3.5.1.a
	\|D3.2		\|D3.2
Line 146:		Line 151:
	\|		\|
	\|-		\|-
			\|rowspan="6"\|Multi-simulation framework development
	\|4.2.1.a		\|4.2.1.a
	\|D4.2		\|D4.2
Line 176:		Line 182:
	\|		\|
	\|-		\|-
			\|rowspan="5"\|Model simulation with ProB
	\|4.3.1.a		\|4.3.1.a
	\|D4.2		\|D4.2
Line 201:		Line 208:
	\|		\|
	\|-		\|-
			\|rowspan="4"\|Model-based testing
	\|4.4.1.a		\|4.4.1.a
	\|D4.3		\|D4.3
Line 221:		Line 229:
	\|		\|
	\|-		\|-
			\|rowspan="4"\|Code generation
	\|4.5.1.a		\|4.5.1.a
	\|D4.2		\|D4.2

imported>Nicolas: /* Task Status */

2013-09-09T13:36:56Z

Task Status

← Older revision		Revision as of 13:36, 9 September 2013
Line 148:		Line 148:
	\|4.2.1.a		\|4.2.1.a
	\|D4.2		\|D4.2
			\|Experimental prototypes
	\|		\|
	\|-		\|-
	\|4.2.1.b		\|4.2.1.b
	\|D4.2		\|D4.2
			\|Support co-simulation of composite system model
	\|		\|
	\|-		\|-
	\|4.2.1.c		\|4.2.1.c
	\|D4.2		\|D4.2
			\|Explore technologies for simulation of continuous models
	\|		\|
	\|-		\|-
	\|4.2.1.d		\|4.2.1.d
	\|D4.2		\|D4.2
			\|Elaborate the specification of the multi-simulation framework
	\|		\|
	\|-		\|-
	\|4.2.2.a		\|4.2.2.a
	\|D4.3		\|D4.3
			\|Develop robust, flexible multi-simulation framework
	\|		\|
	\|-		\|-
	\|4.2.2.b		\|4.2.2.b
	\|D4.4		\|D4.4
			\|Develop guidelines on effective usage of the multi-simulation framework
	\|		\|
	\|-		\|-
	\|4.3.1.a		\|4.3.1.a
	\|D4.2		\|D4.2
			\|Improve scalability of ProB with large hardware: analysis & development
	\|		\|
	\|-		\|-
	\|4.3.1.b		\|4.3.1.b
	\|D4.3		\|D4.3
			\|Improve scalability of ProB with large hardware: performance tuning
	\|		\|
	\|-		\|-
	\|4.3.2.a		\|4.3.2.a
	\|D4.3		\|D4.3
			\|Improve the constraint-solving kernel of ProB
	\|		\|
	\|-		\|-
	\|4.3.3.a		\|4.3.3.a
	\|D4.3		\|D4.3
			\|BMotion Studio support for case studies
	\|		\|
	\|-		\|-
	\|4.3.3.b		\|4.3.3.b
	\|D4.4		\|D4.4
			\|Prototypes for visualisation of large state-spaces and event-trace sets
	\|		\|
	\|-		\|-
	\|4.4.1.a		\|4.4.1.a
	\|D4.3		\|D4.3
			\|Extend Model-based testing framework to accommodate random testing
	\|		\|
	\|-		\|-
	\|4.4.2.a		\|4.4.2.a
	\|D4.3, D4.4		\|D4.3, D4.4
			\|Scenario-based testing
	\|		\|
	\|-		\|-
	\|4.4.3.a		\|4.4.3.a
	\|D4.3		\|D4.3
			\|Coverage detection: specific coverage criteria
	\|		\|
	\|-		\|-
	\|4.4.3.b		\|4.4.3.b
	\|D4.4		\|D4.4
			\|Coverage detection: user annotations
	\|		\|
	\|-		\|-
	\|4.5.1.a		\|4.5.1.a
	\|D4.2		\|D4.2
			\|Enrich the translation rule set from case studies
	\|		\|
	\|-		\|-
	\|4.5.1.b		\|4.5.1.b
	\|D4.3		\|D4.3
			\|Continue to extend translation rule set
	\|		\|
	\|-		\|-
	\|4.5.2.a		\|4.5.2.a
	\|D4.3		\|D4.3
			\|Link code generation to multi-simulation framework
	\|		\|
	\|-		\|-
	\|4.5.3.a		\|4.5.3.a
	\|D4.3		\|D4.3
			\|Generation of stand-alone prototypes
	\|		\|
	\|}		\|}

imported>Nicolas: /* Task Status */

2013-09-09T12:56:01Z

Task Status

@@ Line 142: / Line 142: @@
 |3.5.2.a
 |D3.3
-|Add team working support for merging proofs,
+|Add team working support for comparing and merging proofs,
 model checking, composition and decomposition
+|
 |}

imported>Nicolas: /* Task Status */

2013-09-05T16:29:54Z

Task Status

← Older revision		Revision as of 16:29, 5 September 2013
Line 121:		Line 121:
	\|-		\|-
	\|3.5.1.a		\|3.5.1.a
			\|D3.2
			\|Support for composition and decomposition
	\|		\|
	~~\|Support for composition and decomposition~~
	~~\|D3.2~~
	\|-		\|-
	\|3.5.1.b		\|3.5.1.b