Created
September 9, 2014 19:27
-
-
Save juli1/b107f3c9c5690fd7e543 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
property set POK is | |
Security_Level : aadlinteger applies to | |
(virtual processor, virtual bus, process, bus, event data port, event port, data port); | |
-- Means two things : | |
-- * security_level that a partition is allowed to access | |
-- * security_level provided by a virtual bus : ensure that | |
-- the virtual bus can transport data from and/or to partitions | |
-- that have this security level. | |
Criticality : aadlinteger applies to | |
(virtual processor); | |
-- Represent the criticality level of a partition. | |
Handler : aadlstring applies to | |
(virtual processor); | |
-- Error handler for each partition | |
-- By default, the code generator can create a function | |
-- which name derives from the partition name. Instead, the | |
-- model can provide the name of the handler with this property. | |
Topics : list of aadlstring applies to | |
(virtual processor, virtual bus); | |
-- Means two things : | |
-- * The topics allowed on a specific virtual processor | |
-- * Topics allowed on a virtual bus. | |
Needed_Memory_Size : Size applies to (process); | |
-- Specify the amount of memory needed for a partition | |
-- We apply it to process component because we don't | |
-- isolate virtual processor, only processes | |
Available_Schedulers : type enumeration (RMS, EDF, LLF, RR, TIMESLICE, STATIC); | |
Timeslice : Time applies to (virtual processor); | |
-- DEPRECATED at this time | |
Scheduler : POK::Available_Schedulers | |
applies to (processor, virtual processor); | |
-- List available schedulers | |
-- When we use the STATIC scheduler in the virtual processor | |
-- The Slots and Slots_Allocation properties are used to determine when | |
-- partitions are activated and the timeslice they have for their execution. | |
Available_BSP : type enumeration | |
( | |
x86_qemu, | |
prep, | |
leon3 | |
); | |
BSP : POK::Available_BSP applies to (processor, system); | |
Available_Architectures : type enumeration | |
( | |
x86, ppc, sparc | |
); | |
Architecture : POK::Available_Architectures applies to (processor, system); | |
-- Deployment properties | |
-- Indicate which architecture we use and which bsp | |
MILS_Verified : aadlboolean applies to (system, process, device, thread, processor, data); | |
-- For verification purpose | |
Refresh_Time : Time applies to (data port); | |
Address : aadlstring applies to (device, processor); | |
PCI_Vendor_Id : aadlstring applies to (device); | |
PCI_Device_ID : aadlstring applies to (device); | |
Device_Name : aadlstring applies to (device); | |
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); | |
Des_Key : aadlstring applies to (virtual bus); | |
Des_Init : aadlstring applies to (virtual bus); | |
Blowfish_Key : aadlstring applies to (virtual bus); | |
Blowfish_Init : aadlstring applies to (virtual bus); | |
Supported_POK_Protocols: type enumeration (ceasar,des,blowfish,unknown); | |
Protocol : POK::Supported_POK_Protocols applies to (virtual bus); | |
Supported_Ports_Flush_Time: type enumeration (Major_Frame_Switch, Minor_Frame_Switch, Partition_Slot_Switch); | |
Ports_Flush_Time: POK::Supported_Ports_Flush_Time => Major_Frame_Switch applies to (processor); | |
Module_Minor_Frame: Time applies to (processor); | |
end POK; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
package RAMSES_buses | |
public | |
bus rtl8029 | |
end rtl8029; | |
end RAMSES_buses; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- | |
-- AADL-RAMSES | |
-- | |
-- Copyright © 2012 TELECOM ParisTech and CNRS | |
-- | |
-- TELECOM ParisTech/LTCI | |
-- | |
-- Authors: see AUTHORS | |
-- | |
-- This program is free software: you can redistribute it and/or modify | |
-- it under the terms of the Eclipse Public License as published by Eclipse, | |
-- either version 1.0 of the License, or (at your option) any later version. | |
-- This program is distributed in the hope that it will be useful, | |
-- but WITHOUT ANY WARRANTY; without even the implied warranty of | |
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
-- Eclipse Public License for more details. | |
-- You should have received a copy of the Eclipse Public License | |
-- along with this program. If not, see | |
-- http://www.eclipse.org/org/documents/epl-v10.php | |
-- | |
package RAMSES_processors | |
public | |
with POK; | |
processor cpu_x86 | |
properties | |
POK::Architecture => x86; | |
POK::BSP => x86_qemu; | |
end cpu_x86; | |
end RAMSES_processors; |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment