RESSAC_Use_Case

RESSAC/RESSAC_Use_Case

Fork 0

mirror of http://172.16.200.102/RESSAC/RESSAC_Use_Case.git synced 2025-11-30 20:57:58 +01:00

Files

History

Claire Dross 49c9ca4085 Layer2_MMS_SW_SPARK minor update f_fc.data types

2017-06-20 18:06:14 +02:00

DESIGN.txt

Layer2_MMS_SW_SPARK add parameter items for F_MM

2017-06-20 16:37:50 +02:00

mms-f_el-data.ads

Layer2_MMS_SW_SPARK add parameter items for F_MM

2017-06-20 16:37:50 +02:00

mms-f_el-input.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_el-output.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_el.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_pt-f_cm-input.ads

Take into account Rotactors and use the same type for energy sources

2017-06-16 10:43:34 +02:00

mms-f_pt-f_cm-output.ads

Take into account Rotactors and use the same type for energy sources

2017-06-16 10:43:34 +02:00

mms-f_pt-f_cm.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_pt-f_em-data.ads

Layer2_MMS_SW_SPARK add parameter items for F_MM

2017-06-20 16:37:50 +02:00

mms-f_pt-f_em-input.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_pt-f_em-output.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_pt-f_em.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_pt-f_fc-data.ads

Layer2_MMS_SW_SPARK minor update f_fc.data types

2017-06-20 18:06:14 +02:00

mms-f_pt-f_fc-input.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_pt-f_fc-output.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_pt-f_fc.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_pt-f_mm-behavior-guarantees.adb

Identify entities and supply a SPARK specification for F_MM

2017-06-16 14:43:34 +02:00

mms-f_pt-f_mm-behavior-guarantees.ads

Identify entities and supply a SPARK specification for F_MM

2017-06-16 14:43:34 +02:00

mms-f_pt-f_mm-behavior.ads

Layer2_MMS_SW_SPARK add parameter items for F_MM

2017-06-20 16:37:50 +02:00

mms-f_pt-f_mm-data.ads

Layer2_MMS_SW_SPARK add parameter items for F_MM

2017-06-20 16:37:50 +02:00

mms-f_pt-f_mm-input.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_pt-f_mm-output.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_pt-f_mm.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_pt-input.ads

Take into account Rotactors and use the same type for energy sources

2017-06-16 10:43:34 +02:00

mms-f_pt-output.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-f_pt.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms-input.ads

Take into account Rotactors and use the same type for energy sources

2017-06-16 10:43:34 +02:00

mms-output.ads

List the entities in Ada specification files

2017-06-13 12:44:23 +02:00

mms.ads

Take into account Rotactors and use the same type for energy sources

2017-06-16 10:43:34 +02:00

README.md

add READMEs in new directories

2017-04-25 16:23:42 +02:00

README.md

This folder contains the SPARK version of the software layer development & assurance artefacts for the Mission Management subsystem