Commit 83700a5f authored by jhugues's avatar jhugues

* Update property sets to AADLv2.1

        * Ocarina.Property_Sets: add Modeling_Properties as predefined
          set

        * Ocarina.Instances.Queries: work-around for Get_List_Property
          not returning list in case the list is an enumeration list

        * Update reference outputs



git-svn-id: https://tecsw.estec.esa.int/svn/taste/trunk/ocarina@4964 129961e7-ef38-4bb5-a8f7-c9a525a55882
parent 0e4081f8
model.aadl:85:04: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list.
model.aadl:85:04: Warning: The value of source_language has been converted into a list.
model.aadl:92:04: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list.
model.aadl:92:04: Warning: The value of source_language has been converted into a list.
model.aadl:99:04: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list.
model.aadl:99:04: Warning: The value of source_language has been converted into a list.
pok_safety execution pok_safety execution
requirement : check_error_handling requirement : check_error_handling
------------------------------------- -------------------------------------
......
--****************************************************** --AADL2
-- AADL Standard AADL_V2.0 --SAE Aerospace Standard AS5506A
-- Appendix A (normative) --Proposed Draft (2008-11-08)
-- Predeclared Property Sets --Appendix A: Predeclared Property Sets
-- 07Juin08
--******************************************************
property set AADL_Project is property set AADL_Project is
Supported_Active_Thread_Handling_Protocols: Supported_Active_Thread_Handling_Protocols: type enumeration (abort);
type enumeration (abort,
test); Supported_Connection_Patterns: type enumeration
-- The following are other example protocols. (One_To_One, All_To_All, One_To_All, All_To_One,
-- (complete_one_flush_queue, complete_one_transfer_queue, Next, Previous, Cyclic_Next, Cyclic_Previous);
-- complete_one_preserve_queue, complete_all);
Supported_Concurrency_Control_Protocols: type enumeration
Supported_Connection_Patterns: (None_Specified,
type enumeration ( One_To_One, Interrupt_Masking,
All_To_All, Maximum_Priority,
One_To_All, Immediate_Priority_Ceiling_Protocol,
All_To_One, Protected_Access,
Next, Priority_Inheritance,
Previous, Priority_Ceiling,
Neighbors, Spin_Lock,
All_Neighbors); Semaphore);
-- The Supported_Connection_Patterns property enumeration type
-- specifies the set of patterns that are supported to connect Supported_Dispatch_Protocols: type enumeration (Periodic, Sporadic, Aperiodic, Timed, Hybrid, Background);
-- together a source port array and a destination port array.
Supported_Queue_Processing_Protocols: type enumeration (Fifo);
Supported_Concurrency_Control_Protocols:
type enumeration (NoneSpecified, Supported_Hardware_Source_Languages: type enumeration (VHDL);
Read_Only,
Priority_Inheritance, Supported_Connection_QoS: type enumeration (GuaranteedDelivery, OrderedDelivery, SecureDelivery);
Immediate_Priority_Ceiling_Protocol,
Protected_Access, Supported_Scheduling_Protocols: type enumeration -- Updated for Cheddar
Priority_Ceiling_Protocol, (SporadicServer, RMS, FixedTimeline,
Priority_Ceiling); PARAMETRIC_PROTOCOL,
-- The following are example concurrency control protocols: EARLIEST_DEADLINE_FIRST_PROTOCOL,
-- (Interrupt_Masking, Maximum_Priority, Priority_Inheritance, LEAST_LAXITY_FIRST_PROTOCOL,
-- Priority_Ceiling) RATE_MONOTONIC_PROTOCOL,
DEADLINE_MONOTONIC_PROTOCOL,
Supported_Dispatch_Protocols: ROUND_ROBIN_PROTOCOL,
type enumeration (Periodic, TIME_SHARING_BASED_ON_WAIT_TIME_PROTOCOL,
Aperiodic, POSIX_1003_HIGHEST_PRIORITY_FIRST_PROTOCOL,
Sporadic, D_OVER_PROTOCOL,
Timed, MAXIMUM_URGENCY_FIRST_BASED_ON_LAXITY_PROTOCOL,
Hybrid, MAXIMUM_URGENCY_FIRST_BASED_ON_DEADLINE_PROTOCOL,
Background); TIME_SHARING_BASED_ON_CPU_USAGE_PROTOCOL,
-- The following are protocols for which the semantics are defined: NO_SCHEDULING_PROTOCOL,
-- (Periodic, Sporadic, Aperiodic, Timed, Hybrid, Background); HIERARCHICAL_CYCLIC_PROTOCOL,
HIERARCHICAL_ROUND_ROBIN_PROTOCOL,
Supported_Hardware_Source_Languages: HIERARCHICAL_FIXED_PRIORITY_PROTOCOL,
type enumeration (VHDL); HIERARCHICAL_PARAMETRIC_PROTOCOL);
-- The following is an example hardware description language:
-- (VHDL) Supported_Source_Languages: type enumeration -- Updated for TASTE/Ocarina
-- XXX FIX ADD WAITING Peter FEILER
Supported_Queue_Processing_Protocols: type enumeration
(FIFO);
-- The Supported_Queue_Processing_Protocols property enumeration
-- type specifies the set of queue processing protocols that are
-- supported.
Supported_Connection_QoS :
type enumeration (GuaranteedDelivery,
OrderedDelivery,
SecureDelivery);
-- The Supported_QoS property specifies the quality of services .
Supported_Scheduling_Protocols: type enumeration
(PARAMETRIC_PROTOCOL,
EARLIEST_DEADLINE_FIRST_PROTOCOL,
LEAST_LAXITY_FIRST_PROTOCOL,
RATE_MONOTONIC_PROTOCOL,
DEADLINE_MONOTONIC_PROTOCOL,
ROUND_ROBIN_PROTOCOL,
TIME_SHARING_BASED_ON_WAIT_TIME_PROTOCOL,
POSIX_1003_HIGHEST_PRIORITY_FIRST_PROTOCOL,
D_OVER_PROTOCOL,
MAXIMUM_URGENCY_FIRST_BASED_ON_LAXITY_PROTOCOL,
MAXIMUM_URGENCY_FIRST_BASED_ON_DEADLINE_PROTOCOL,
TIME_SHARING_BASED_ON_CPU_USAGE_PROTOCOL,
NO_SCHEDULING_PROTOCOL,
HIERARCHICAL_CYCLIC_PROTOCOL,
HIERARCHICAL_ROUND_ROBIN_PROTOCOL,
HIERARCHICAL_FIXED_PRIORITY_PROTOCOL,
HIERARCHICAL_PARAMETRIC_PROTOCOL);
-- The following are examples of scheduling protocols:
-- (RMS, EDF, Sporadicserver, SlackServer, ARINC653)
Supported_Source_Languages: type enumeration
(Ada95, (Ada95,
Ada, -- alias for Ada95 Ada, -- alias for Ada95
Ada05, -- alias for Ada95 Ada05, -- alias for Ada95
ASN1, ASN1,
Blackbox_Device, Blackbox_Device,
C, C,
CPP, -- C++ CPP, -- C++
Esterel, Esterel,
GUI, GUI,
LUA, LUA,
...@@ -115,28 +77,23 @@ property set AADL_Project is ...@@ -115,28 +77,23 @@ property set AADL_Project is
VHDL, VHDL,
ACN); ACN);
Supported_Distributions: type enumeration (Fixed); Supported_Distributions: type enumeration (Fixed, Poisson);
-- The following are example distributions:
-- ( Fixed, Poisson )
Data_Volume: type aadlinteger 0 bitsps .. Max_Aadlinteger Supported_Classifier_Substitutions: type enumeration (Classifier_Match, Type_Extension, Signature_Match);
units ( bitsps,
Bytesps => bitsps * 8,
KBytesps => Bytesps * 1000,
MBytesps => KBytesps * 1000,
GBytesps => MBytesps * 1000 );
-- The Data_Volume property type specifies a property type for the
-- volume of data per time unit. The predeclared unit literals are
-- expressed in terms of seconds as time unit. The numeric value
-- of the property must be positive.
Max_Aadlinteger: constant aadlinteger => 2#1#e61;
Data_Volume: type aadlinteger 0 bitsps .. Max_Data_Volume
units Data_Volume_Units;
Max_Data_Volume: constant aadlinteger units Data_Volume_Units => 2#1#e62 bitsps; -- XXX extended
Max_Aadlinteger: constant aadlinteger => 2#1#e32;
Max_Target_Integer: constant aadlinteger => 2#1#e32; Max_Target_Integer: constant aadlinteger => 2#1#e32;
Max_Base_Address: constant aadlinteger => 2#1#e32; Max_Base_Address: constant aadlinteger => 2#1#e32;
Max_Memory_Size: constant Size => 2#1#e48 Bytes; Max_Memory_Size: constant Size => 2#1#e32 Bytes;
Max_Queue_Size: constant aadlinteger => 512; Max_Queue_Size: constant aadlinteger => 512;
...@@ -146,27 +103,32 @@ property set AADL_Project is ...@@ -146,27 +103,32 @@ property set AADL_Project is
Max_Urgency: constant aadlinteger => 12; Max_Urgency: constant aadlinteger => 12;
Max_Word_Count: constant aadlinteger => 2#1#e32; Max_Byte_Count: constant aadlinteger => 2#1#e32;
Max_Word_Space: constant aadlinteger => 64; Max_Word_Space: constant aadlinteger => 64;
Size_Units: type units ( Size_Units: type units (
bits, bits,
Bytes => bits * 8, Bytes => bits * 8,
KByte => Bytes * 1000, KByte => Bytes * 1000,
MByte => KByte * 1000, MByte => KByte * 1000,
GByte => MByte * 1000, GByte => MByte * 1000,
TByte => GByte * 1000); TByte => GByte * 1000);
-- Note: B, KB, etc. in AADL 2004 have been replaced by Byte, Kbyte
-- etc. in AADL V2.
Time_Units: type units ( Time_Units: type units (
ps, ps,
ns => ps * 1000, ns => ps * 1000,
us => ns * 1000, us => ns * 1000,
ms => us * 1000, ms => us * 1000,
sec => ms * 1000, sec => ms * 1000,
min => sec * 60, min => sec * 60,
hr => min * 60); hr => min * 60);
Data_Volume_Units: type units (
bitsps,
Bytesps => bitsps * 8,
KBytesps => Bytesps * 1000,
MBytesps => KBytesps * 1000,
GBytesps => MBytesps * 1000);
end AADL_Project; end AADL_Project;
...@@ -2,7 +2,6 @@ ...@@ -2,7 +2,6 @@
-- used as part of the ASSERT process. -- used as part of the ASSERT process.
package ASSERT_Types package ASSERT_Types
public public
with Data_Model; with Data_Model;
......
--****************************************************** --AADL2
-- AADL Standard AADL_V2.0 --SAE Aerospace Standard AS5506A
-- Appendix A (normative) --Proposed Draft (2008-11-08)
-- Predeclared Property Sets --Appendix A: Predeclared Property Sets
-- Communication_Properties
-- 07Juin08
--******************************************************
property set Communication_Properties is property set Communication_Properties is
---------------------------------------------------- Fan_Out_Policy: enumeration (Broadcast, RoundRobin, Selective, OnDemand)
---------------------------------------------------- applies to (port);
Fan_Out_Policy: enumeration (Broadcast, -- XXX not supported by Ocarina
RoundRobin, -- Connection_Pattern: list of list of Supported_Connection_Patterns
OnDemand) -- applies to (connection);
applies to (port);
---------------------------------------------------- -- Connection_Set: list of Connection_Pair
-- applies to (connection);
Connection_Pattern:
list of Supported_Connection_Patterns -- Connection_Pair: type record (
applies to (connection); -- src: list of aadlinteger;
---------------------------------------------------- -- dst: list of aadlinteger;);
Connection_Set: list of Connection_Pair Overflow_Handling_Protocol: enumeration (DropOldest, DropNewest, Error) => DropOldest
applies to (connection); applies to (event port, event data port, subprogram access);
----------------------------------------------------
Queue_Processing_Protocol: Supported_Queue_Processing_Protocols => FIFO
Connection_Pair: applies to (event port, event data port, subprogram access);
type record ( src: aadlinteger;
dst: aadlinteger;); Queue_Size: aadlinteger 0 .. Max_Queue_Size => 1
applies to (event port, event data port, subprogram access);
----------------------------------------------------
Overflow_Handling_Protocol: enumeration (DropOldest, Required_Connection: aadlboolean => true
DropNewest, applies to (feature);
Error)
=> DropOldest Timing: enumeration (sampled, immediate, delayed) => sampled
applies to (event port, applies to (port connection);
event data port,
subprogram); Transmission_Type: enumeration (push, pull)
---------------------------------------------------- applies to (data port, port connection, bus, virtual bus);
Queue_Processing_Protocol: Input_Rate: Rate_Spec => (Value_Range => 1.0 .. 1.0; Rate_Unit => PerDispatch; Rate_Distribution => Fixed;)
Supported_Queue_Processing_Protocols applies to (port);
=> FIFO
applies to (event port, Input_Time: list of IO_Time_Spec => ((Time => Dispatch; Offset => 0 ns .. 0 ns;))
event data port, applies to (port);
subprogram);
---------------------------------------------------- IO_Time_Spec: type record (
Offset: Time_Range;
Queue_Size: aadlinteger 0 .. Max_Queue_Size => 0 Time: IO_Reference_Time;
applies to (event port, );
event data port,
subprogram); IO_Reference_Time: type enumeration (Dispatch, Start, Completion, Deadline, NoIO);
----------------------------------------------------
Output_Rate: Rate_Spec => (Value_Range => 1.0 .. 1.0; Rate_Unit => PerDispatch; Rate_Distribution => Fixed;)
Transmission_Type: enumeration ( push, pull ) applies to (port);
applies to (port,
connection, Output_Time: list of IO_Time_Spec => ((Time => Completion; Offset => 0 ns .. 0 ns;))
bus, applies to (port);
virtual bus);
---------------------------------------------------- Rate_Spec: type record (
Value_Range: range of aadlreal;
Input_Rate: Rate_Spec Rate_Unit: enumeration (PerSecond, PerDispatch);
applies to (port, access); Rate_Distribution: Supported_Distributions;
---------------------------------------------------- );
Input_Time: IO_Time_Spec Subprogram_Call_Rate: Rate_Spec => (Value_Range => 1.0 .. 1.0; Rate_Unit => PerDispatch; Rate_Distribution => Fixed;)
applies to (port, access); applies to (subprogram access);
----------------------------------------------------
Transmission_Time: record (
IO_Time_Spec : type record ( Fixed: Time_Range;
ReferencePoint : IO_Reference_Point_Type; PerByte: Time_Range;)
TimeOffset : TimeRange; applies to (bus);
);
---------------------------------------------------- Actual_Latency: Time_Range
applies to (flow, connection, bus, processor, device, port);
IO_Reference_Point_Type :
type enumeration ( DispatchTime, Latency: Time_Range
StartTime, applies to (flow, connection, bus, processor, device, port);
CompletionTime,
DeadlineTime,
NoIO);
----------------------------------------------------
Output_Rate: Rate_Spec
applies to (port, access);
----------------------------------------------------
Output_Time: IO_Time_Spec
applies to (port, access);
----------------------------------------------------
-- XXX FIX : TO BE CHANGE BY FEILER
-- Rate_Spec : type record (
-- Value_Range : aadlreal units (perSecond, perDispatch);
-- Rate_Distribution : Supported_Distributions;
-- );
Rate_Spec : type record (rec: aadlinteger;);
----------------------------------------------------
Transmission_Time: list of Time_Range
applies to (bus);
----------------------------------------------------
Actual_Latency: Time_Range
applies to (flow);
----------------------------------------------------
Expected_Latency: Time_Range
applies to (flow);
----------------------------------------------------
Latency: Time_Range
applies to (flow, connection);
----------------------------------------------------
----------------------------------------------------
end Communication_Properties; end Communication_Properties;
\ No newline at end of file
--****************************************************** --AADL2
-- AADL Standard AADL_V2.0 --SAE Aerospace Standard AS5506A
-- Appendix A (normative) --Proposed Draft (2008-11-08)
-- Predeclared Property Sets --Appendix A: Predeclared Property Sets
-- Deployment_Properties
-- 07Juin08
--******************************************************
property set Deployment_Properties is property set Deployment_Properties is
---------------------------------------------------- Allowed_Processor_Binding_Class:
---------------------------------------------------- inherit list of classifier (processor, virtual processor, system)
applies to (thread, thread group, process, system, virtual processor, device);
Device_Driver: classifier (abstract) applies to (device);
Allowed_Processor_Binding: inherit list of reference (processor, virtual processor, system)
Allowed_Processor_Binding_Class: applies to (thread, thread group, process, system, virtual processor, device);
inherit list of classifier (processor,
virtual processor, Actual_Processor_Binding: inherit list of reference (processor, virtual processor)
system) applies to (thread, thread group, process, system, virtual processor, device);
applies to (thread,
thread group, Allowed_Memory_Binding_Class:
process, inherit list of classifier (memory, system, processor)
system, applies to (thread, thread group, process, system, device, data, data port, event data port, subprogram, subprogram group, processor);
virtual processor,
device); Allowed_Memory_Binding: inherit list of reference (memory, system, processor)
---------------------------------------------------- applies to (thread, thread group, process, system, device, data, data port, event data port, subprogram, subprogram group, processor);
Allowed_Processor_Binding: Actual_Memory_Binding: inherit list of reference (memory)
inherit list of reference (processor, applies to (thread, thread group, process, system, processor, device, data, data port, event data port, subprogram, subprogram group);
virtual processor,
system) Allowed_Connection_Binding_Class:
applies to (thread, inherit list of classifier (processor, virtual processor, bus, virtual bus, device, memory)
thread group, applies to (feature, connection, thread, thread group, process, system, virtual bus);
process,
system, Allowed_Connection_Binding: inherit list of reference (processor, virtual processor, bus, virtual bus, device, memory)
virtual processor, applies to (feature, connection, thread, thread group, process, system, virtual bus);
device);
---------------------------------------------------- Actual_Connection_Binding: inherit list of reference (processor, virtual processor, bus, virtual bus, device, memory)
applies to (feature, connection, thread, thread group, process, system, virtual bus);
Actual_Processor_Binding:
inherit list of reference (processor, Allowed_Subprogram_Call: list of reference (subprogram)
virtual processor) applies to (subprogram access);
applies to (thread,
thread group, Actual_Subprogram_Call: reference (subprogram)
process, applies to (subprogram access);
system,
virtual processor, Allowed_Subprogram_Call_Binding:
device); list of reference (bus, processor, device)
---------------------------------------------------- applies to (subprogram, thread, thread group, process, system);
Allowed_Memory_Binding_Class: Actual_Subprogram_Call_Binding: list of reference (bus, processor, memory, device)
inherit list of classifier (memory, applies to (subprogram);
system,
processor) Provided_Virtual_Bus_Class: inherit list of classifier (virtual bus)
applies to (thread, applies to (bus, virtual bus, processor, virtual processor, device, memory, system);
thread group,
process, Required_Virtual_Bus_Class: inherit list of classifier (virtual bus)
system, applies to (virtual bus, connection, port, thread, thread group, process, system, device);
device,
data, Provided_Connection_Quality_Of_Service: inherit list of Supported_Connection_QoS
data port, applies to (bus, virtual bus, processor, virtual processor, system, device, memory);
event data port,
subprogram, Required_Connection_Quality_Of_Service: inherit list of Supported_Connection_QoS
processor); applies to (port, connection, virtual bus, thread, thread group, process, system, device);
----------------------------------------------------
-- XXX not supported by Ocarina
Allowed_Memory_Binding: -- Not_Collocated: record ( Targets: list of reference (data,
inherit list of reference (memory, -- thread, process, system, connection); Location:
system, -- classifier (processor, memory, bus, system);) applies
processor) -- to (process, system);
applies to (thread,
thread group, -- Collocated: record ( Targets: list of reference (data, thread,
process, -- process, system, connection); Location: classifier
system, -- (processor, memory, bus, system);) applies to
device, -- (process, system);
data,
data port, Allowed_Connection_Type: list of enumeration
event data port, (Sampled_Data_Connection, Immediate_Data_Connection,
subprogram, Delayed_Data_Connection, Port_Connection,
processor); Data_Access_Connection,
---------------------------------------------------- Subprogram_Access_Connection)
applies to (bus, device);
Actual_Memory_Binding:
inherit list of reference (memory) Allowed_Dispatch_Protocol: list of Supported_Dispatch_Protocols
applies to (thread, applies to (processor, virtual processor);
thread group,
process, Allowed_Period: list of Time_Range
system, applies to (processor, system, virtual processor);
processor,
device, Allowed_Physical_Access_Class: list of classifier (device, processor, memory, bus)
data, applies to (bus);
data port,
event data port, Allowed_Physical_Access: list of reference (device, processor, memory, bus)
feature group, applies to (bus);
subprogram);
---------------------------------------------------- Memory_Protocol: enumeration (execute_only, read_only, write_only, read_write) => read_write
applies to (memory);
Allowed_Connection_Binding_Class:
inherit list of classifier(processor, Runtime_Protection_Support : aadlboolean
virtual processor, applies to (processor, virtual processor);
bus,
virtual bus, Scheduling_Protocol: inherit list of Supported_Scheduling_Protocols
device, applies to (virtual processor, processor);
memory)
applies to (port, Preemptive_Scheduler: aadlboolean
connection, applies to (processor);
thread,
thread group,