Commit 8b1a9bdb authored by yoogx's avatar yoogx

Merge branch 'master' of https://github.com/yoogx/ocarina

parents 388c01b9 3823e343
......@@ -135,8 +135,8 @@ install-data-local: all
fi
$(INSTALL_DATA) $(srcdir)/CONTRIBUTING $(DESTDIR)$(datadir)/doc/ocarina
$(INSTALL_DATA) $(srcdir)/PROBLEM-REPORT-FORM $(DESTDIR)$(datadir)/doc/ocarina
$(INSTALL_DATA) $(builddir)/ocarina-config.html $(DESTDIR)$(datadir)/doc/ocarina
$(INSTALL_DATA) $(builddir)/ocarina_man.html $(DESTDIR)$(datadir)/doc/ocarina
$(INSTALL_DATA) $(srcdir)/ocarina-config.html $(DESTDIR)$(datadir)/doc/ocarina
$(INSTALL_DATA) $(srcdir)/ocarina_man.html $(DESTDIR)$(datadir)/doc/ocarina
$(INSTALL_DATA) $(srcdir)/ocarina.css $(DESTDIR)$(datadir)/doc/ocarina
uninstall-local:
......
-- This property set is derived from the Behavior Annex language
-- specification, as part of the AS5506/2 standard.
property set Behavior_Properties is
Subprogram_Call_Protocol: enumeration (HSER,LSER,ASER) => HSER
applies to (subprogram access);
-- The Behavior Annex introduces more precise communication
-- protocols that can be used to better control the blocking
-- duration of a client thread during a remote call to a server
-- thread. These protocols are derived from the main HOOD
-- functional execution requests:
-- * HSER for Highly Synchronous Execution Request.
-- * LSER for Loosely Synchronous Execution Request.
-- * ASER for ASynchronous Execution Request.
end Behavior_Properties;
--EMV2.aadl
property set EMV2
is
OccurrenceDistribution : EMV2::DistributionSpecification
applies to ({emv2}**error propagation, {emv2}**error flow, {emv2}**error behavior event
,{emv2}**error behavior state,{emv2}**error type,{emv2}**type set);
--needed to separate the property "Occurrence" from its type declaration
--so other properties may have that type
DistributionSpecification : type record (
ProbabilityValue : aadlreal;
OccurrenceRate : aadlreal;
MeanValue : aadlreal;
StandardDeviation : aadlreal;
ShapeParameter : aadlreal;
ScaleParameter : aadlreal;
SuccessCount : aadlreal;
SampleCount : aadlreal;
Probability : aadlreal;
Distribution : EMV2::DistributionFunction;);
--Fixed represents a fixed distribution and takes a single parameter OccurrenceRate or ProbabilityValue.
--Poisson aka. Exponential represents an exponential distribution and takes a single parameter OccurrenceRate or ProbabilityValue.
--Normal aka. Gauss represents a distribution with an explicitly specified MeanValue and StandardDeviation.
--Weibull represents a shaped distribution with a ShapeParameter and a ScaleParameter.
--Binominal represents represents a discrete distribution with a SuccessCount, a SampleCount, and a Probability parameter.
DistributionFunction : type enumeration (Fixed, Poisson, Exponential, Normal, Gauss, Weibull, Binominal);
DurationDistributionSpecification : type record (
Duration : Time_Range;
Distribution : EMV2::DistributionFunction;);
DurationDistribution : EMV2::DurationDistributionSpecification applies to ({emv2}**Repair Event, {emv2}**Recover Event,
{emv2}**Error Behavior Transition);
-- A PropagationTimeDelay property indicates the delay in propagating and error as a distribution over a time interval.
-- For example, as a property associated with a connection it indicates the time delay of the error propagation.
PropagationTimeDelay: EMV2::DurationDistributionSpecification
applies to (connection, {emv2}**propagation path);
StateKind : EMV2::StateKindEnum
applies to ({emv2}**error behavior state);
StateKindEnum: type enumeration (Working, NonWorking);
-- Indicates whether an error type is detectable
DetectionMechanism : aadlstring
applies to ({emv2}**error detection);
-- The FaultKind property allows the user to specify whether an error source,
-- i.e., the occurrence of a fault activation or a propagation is due to a design fault or an operational fault.
-- Design faults are faults that could be eliminated at design time, but if present result in an error.
-- Operational faults are faults that inherently occur during operation and should be detected and managed during operation.
FaultKind : EMV2::FaultKindEnum
applies to ( {emv2}**error event, {emv2}**error propagation, {emv2}**error source, {emv2}**error type, {emv2}**type set);
FaultKindEnum: type enumeration (Design, Operational);
-- The Persistence property allows the user to specify whether an error is permanent, transient, or a singleton.
-- A permanent error typically requires a repair action to the component with the fault occurrence.
-- A transient error has a limited duration and typically requires a recovery action.
-- In a discrete event system a transient error may last over several discrete events, e.g., a corrupted message may be sent over multiple periods.
-- A singleton error occurs in the context of a single discrete event. For example, a divide by zero error may be specific to a computation on a particular input.
Persistence : EMV2::PersistenceEnum
applies to ({emv2}**error type, {emv2}**type set, {emv2}**error behavior state,
{emv2}**error behavior event, {emv2}**error propagation);
PersistenceEnum: type enumeration (Permanent, Transient, Singleton);
-- The severity property value indicates the severity of the hazard ranging from 1 (high) to 5 (low).
-- MIL-STD 882D refers to it as SeverityCategory with equivalent descriptive labels as SeverityLevel.
-- Qualify these labels (Catastrophic, Critical, Marginal, Negligible) with MILSTD882::
-- ARP 4761 calls this SeverityClassification with descriptive labels
-- (Catastrophic, Hazardous, Major, Minor, NoEffect) (qualify with ARP4761::).
Severity : inherit EMV2::SeverityRange applies to ({emv2}**error type, {emv2}**type set, {emv2}**error behavior state,
{emv2}**error source, {emv2}**error propagation, {emv2}**error event);
SeverityRange: type aadlinteger 1 .. 5;
ProbabilityRange: type aadlreal 0.0 .. 1.0;
-- The likelihood property value indicates the likelihood of the hazard ranging from A (high) to E (low).
-- MIL-STD 882D uses descriptive labels (Frequent, Probable, Occasional, Remote, Improbable) (See property set MILSTD882).
-- ARP 4761 uses descriptive labels (Frequent, Probable, Remote, ExtremelyRemote, ExtremelyImprobable) (See property set ARP4761).
Likelihood : inherit EMV2::LikelihoodLabels applies to ({emv2}**error type, {emv2}**type set, {emv2}**error behavior state,
{emv2}**error source, {emv2}**error propagation, {emv2}**error event);
LikelihoodLabels: type enumeration (A, B, C, D, E);
-- ARP4761-style labels for likelihood: qualify with ARP4761::
-- Frequent, Probable, Occasional, Remote, Improbable
-- MILSTD882-style labels for likelihood: qualify with MILSTD882::
-- Frequent, Probable, Remote, ExtremelyRemote, ExtremelyImprobable
DALLabels: type enumeration (A,B,C,D,E);
Hazards: list of record
(
CrossReference : aadlstring; -- cross reference to an external document
HazardTitle : aadlstring; -- short descriptive phrase for hazard
Description : aadlstring; -- description of the hazard (same as hazardtitle)
Failure : aadlstring; -- system deviation resulting in failure effect
FailureEffect : aadlstring; -- description of the effect of a failure (mode)
Phases : list of aadlstring; -- operational phases in which the hazard is relevant
Environment : aadlstring; -- description of operational environment
Mishap : aadlstring; -- description of event (series) resulting in
-- unintentional death, etc.(MILSTD882)
FailureCondition : aadlstring; -- description of event (series) resulting in
-- unintentional death, etc.(ARP4761)
Risk : aadlstring; -- description of risk. Risk is characterized by
-- severity, likelihood, and occurrence probability
Severity : EMV2::SeverityRange ; -- actual risk as severity
Likelihood : EMV2::LikelihoodLabels; -- actual risk as likelihood/probability
Probability: EMV2::ProbabilityRange; -- probability of a hazard
TargetSeverity : EMV2::SeverityRange; -- acceptable risk as severity
TargetLikelihood : EMV2::LikelihoodLabels; -- acceptable risk as likelihood/prob
DevelopmentAssuranceLevel : EMV2::DALLabels; -- level of rigor in development
-- assurance (ARP4761)
VerificationMethod : aadlstring; -- verification method to address the hazard
SafetyReport : aadlstring; -- analysis/assessment of hazard
Comment : aadlstring;
)
applies to ({emv2}**error type, {emv2}**type set, {emv2}**error behavior state,
{emv2}**error source, {emv2}**error propagation, {emv2}**error event);
Description : aadlstring applies to (all);
HazardAllocation: record (
AssumedProbability : aadlreal;
ExposureTime : Time;
Notes : aadlstring;
) applies to (all);
end EMV2;
......@@ -73,6 +73,7 @@ property set POK is
Available_BSP : type enumeration
(
x86_qemu,
x86_qemu_vmm,
prep,
leon3
);
......@@ -110,7 +111,7 @@ property set POK is
Additional_Features : list of POK::Supported_Additional_Features applies to (virtual processor, processor);
Supported_Additional_Features: type enumeration (libmath, libc_stdlib, libc_stdio, libc_string, io, pci, console, libc);
Supported_Additional_Features: type enumeration (libmath, libc_stdlib, libc_stdio, libc_string, io, pci, console, libc, x86_vmm);
Des_Key : aadlstring applies to (virtual bus);
......
......@@ -17,7 +17,9 @@ AADL_V2_PROPERTIES = $(srcdir)/AADLv2/aadl_project.aadl \
$(srcdir)/AADLv2/arinc653_properties.aadl \
$(srcdir)/AADLv2/assert_types.aadl \
$(srcdir)/AADLv2/assert_properties.aadl \
$(srcdir)/AADLv2/behavior_properties.aadl \
$(srcdir)/AADLv2/deployment_properties.aadl \
$(srcdir)/AADLv2/emv2.aadl \
$(srcdir)/AADLv2/Cheddar_Properties.aadl \
$(srcdir)/AADLv2/thread_properties.aadl \
$(srcdir)/AADLv2/communication_properties.aadl \
......
......@@ -1224,6 +1224,32 @@ package body Ocarina.Backends.POK_C.Deployment is
Set_Deployment_Header;
end if;
if Get_Name_String
(ATN.Name
(ATN.Identifier (S))) = "x86_vmm"
then
CTU.Pop_Entity;
CTU.Pop_Entity;
Push_Entity (Kernel_Unit);
Set_Deployment_Header;
N := CTU.Make_Define_Statement
(Defining_Identifier =>
RE (RE_Pok_Needs_X86_Vmm),
Value => CTU.Make_Literal
(CV.New_Int_Value (1, 1, 10)));
CTU.Append_Node_To_List
(N, CTN.Declarations (CTU.Current_File));
Pop_Entity;
CTU.Push_Entity (P);
CTU.Push_Entity (U);
Set_Deployment_Header;
end if;
S := ATN.Next_Node (S);
end loop;
......
......@@ -658,6 +658,8 @@ package body Ocarina.Backends.POK_C.Makefile is
case BSP is
when POK_BSP_x86_qemu =>
Write_Line ("export BSP=x86-qemu");
when POK_BSP_x86_qemu_vmm =>
Write_Line ("export BSP=x86-qemu-vmm");
when POK_BSP_Leon =>
Write_Line ("export BSP=leon3");
when POK_BSP_prep =>
......
......@@ -204,6 +204,7 @@ package Ocarina.Backends.POK_C.Runtime is
RE_Pok_Needs_Ports_Virtual, -- POK_NEEDS_PORTS_VIRTUAL
RE_Pok_Needs_Gettick, -- POK_NEEDS_GETTICK
RE_Pok_Needs_Ports_Queueing, -- POK_NEEDS_PORTS_QUEUEING
RE_Pok_Needs_X86_Vmm, -- POK_NEEDS_X86_VMM
RE_Pok_Errno_Empty, -- POK_ERRNO_EMPTY
RE_Pok_Errno_Ok, -- POK_ERRNO_OK
RE_Pok_Hw_Addr, -- POK_HW_ADDR
......@@ -712,6 +713,7 @@ package Ocarina.Backends.POK_C.Runtime is
RE_Pok_Needs_Ports_Virtual => RH_Deployment,
RE_Pok_Needs_Gettick => RH_Null,
RE_Pok_Needs_Ports_Queueing => RH_Deployment,
RE_Pok_Needs_X86_Vmm => RH_Deployment,
RE_Pok_Errno_Empty => RH_Errno,
RE_Pok_Errno_Ok => RH_Errno,
RE_Pok_Hw_Addr => RH_Deployment,
......
......@@ -366,6 +366,7 @@ package body Ocarina.Backends.Properties is
POK_Arch_x86_Name : Name_Id;
POK_BSP_x86_qemu_Name : Name_Id;
POK_BSP_x86_qemu_vmm_Name : Name_Id;
POK_Arch_Sparc_Name : Name_Id;
POK_BSP_Leon_Name : Name_Id;
POK_Arch_ppc_Name : Name_Id;
......@@ -3485,6 +3486,7 @@ package body Ocarina.Backends.Properties is
POK_Arch_x86_Name := Get_String_Name ("x86");
POK_BSP_x86_qemu_Name := Get_String_Name ("x86_qemu");
POK_BSP_x86_qemu_vmm_Name := Get_String_Name ("x86_qemu_vmm");
POK_Arch_Sparc_Name := Get_String_Name ("sparc");
POK_BSP_Leon_Name := Get_String_Name ("leon3");
POK_Arch_ppc_Name := Get_String_Name ("ppc");
......@@ -3631,6 +3633,8 @@ package body Ocarina.Backends.Properties is
if P_Name = POK_BSP_x86_qemu_Name then
return POK_BSP_x86_qemu;
elsif P_Name = POK_BSP_x86_qemu_vmm_Name then
return POK_BSP_x86_qemu_vmm;
elsif P_Name = POK_BSP_prep_Name then
return POK_BSP_prep;
elsif P_Name = POK_BSP_Leon_Name then
......
......@@ -116,6 +116,7 @@ package Ocarina.Backends.Properties is
type Supported_POK_BSP is
(POK_BSP_x86_qemu,
POK_BSP_x86_qemu_vmm,
POK_BSP_Leon,
POK_BSP_prep,
Invalid_BSP);
......
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2009 Telecom ParisTech, 2010-2012 ESA & ISAE. --
-- Copyright (C) 2009 Telecom ParisTech, 2010-2014 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify --
-- it under terms of the GNU General Public License as published by the --
......@@ -658,12 +658,19 @@ package body Ocarina.Analyzer.AADL.Semantics is
(Category (Connection_Source)) = CC_Data);
Bus_And_Require_Bus_Access :=
Kind (Connection_Source) = K_Subcomponent
(Kind (Connection_Source) = K_Subcomponent
and then Component_Category'Val (Category
(Connection_Source)) = CC_Bus
and then Kind (Connection_Destination) = K_Subcomponent_Access
and then Component_Category'Val
(Subcomponent_Category (Connection_Destination)) = CC_Bus;
(Subcomponent_Category (Connection_Destination)) = CC_Bus)
or else
(Kind (Connection_Source) = K_Subcomponent_Access
and then Component_Category'Val (Subcomponent_Category
(Connection_Source)) = CC_Bus
and then Kind (Connection_Destination) = K_Subcomponent
and then Component_Category'Val
(Category (Connection_Destination)) = CC_Bus);
Provide_Bus_Access_And_Bus :=
(Kind (Connection_Destination) = K_Subcomponent_Access
......@@ -941,7 +948,7 @@ package body Ocarina.Analyzer.AADL.Semantics is
Directions := True;
else
Directions := ((not Source_Is_Local)
and then (not Destination_Is_Local)
and then (not Destination_Is_Local)
and then Is_Out (Connection_Source)
and then Is_In (Connection_Destination))
or else (Source_Is_Local
......@@ -970,6 +977,8 @@ package body Ocarina.Analyzer.AADL.Semantics is
when K_Subcomponent_Access =>
Directions :=
Is_Bidirectional (Node)
or else
(not Source_Is_Local
and then not Destination_Is_Local
and then not Is_Provided (Connection_Destination)
......@@ -995,7 +1004,7 @@ package body Ocarina.Analyzer.AADL.Semantics is
and then Kind (Connection_Source) = K_Subcomponent);
when K_Subcomponent =>
Directions := False;
Directions := Is_Bidirectional (Node);
when others =>
Directions := True;
......
......@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2012 ESA & ISAE. --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2014 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify --
-- it under terms of the GNU General Public License as published by the --
......@@ -132,7 +132,10 @@ package Ocarina.ME_AADL.AADL_Tree.Entities.Properties is
PO_Provides_Subprogram_Access,
PO_Prototype,
PO_Package);
PO_Package,
PO_Alien_Meta_Model -- Not support alien meta-model elements, e.g. EMV2
);
type Referable_Element_Category is
(REC_Component_Category,
......
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2012 ESA & ISAE. --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2014 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify --
-- it under terms of the GNU General Public License as published by the --
......@@ -981,10 +981,12 @@ package body Ocarina.FE_AADL.Lexer is
-- Skip_Tokens --
-----------------
procedure Skip_Tokens (Delimiters : Token_List_Type) is
procedure Skip_Tokens (Delimiters : Token_List_Type;
Include_Delimiter : Boolean := True)
is
begin
for Index in Delimiters'Range loop
Skip_Tokens (Delimiters (Index));
Skip_Tokens (Delimiters (Index), Include_Delimiter);
end loop;
end Skip_Tokens;
......
......@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2012 ESA & ISAE. --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2014 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify --
-- it under terms of the GNU General Public License as published by the --
......@@ -86,7 +86,8 @@ package Ocarina.FE_AADL.Lexer is
-- Skip tokens until we find Delimiter
-- This procedure verifies that skipped tokens are well embraced
procedure Skip_Tokens (Delimiters : Token_List_Type);
procedure Skip_Tokens (Delimiters : Token_List_Type;
Include_Delimiter : Boolean := True);
-- Same as above, with each token T in given list, calls Skip_Tokens (T)
end Ocarina.FE_AADL.Lexer;
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2012 ESA & ISAE. --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2014 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify --
-- it under terms of the GNU General Public License as published by the --
......@@ -2918,6 +2918,14 @@ package body Ocarina.FE_AADL.Parser.Properties.Values is
Owner_Category := New_Node (K_Named_Element, Token_Location);
case Token is
when T_Left_Curly_Bracket =>
-- For now, we simply skip annex-dependent properties
Save_Lexer (Loc);
Skip_Tokens ((T_Comma, T_Right_Parenthesis), False);
Category := PO_Alien_Meta_Model;
Comp_Cat := CC_Unknown;
when T_Abstract | T_System
| T_Processor | T_Thread
| T_Process | T_Virtual
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment