From 57f39581892965a95b0a7054fb3fc3c994e34c06 Mon Sep 17 00:00:00 2001 From: yoogx Date: Fri, 9 Sep 2016 11:26:26 +0200 Subject: [PATCH] * Addition of the Alloy library For issue #68 --- configure.ac | 1 + resources/runtime/Makefile.am | 2 +- resources/runtime/alloy/Makefile.am | 16 + .../analysis/example_scheduling_analysis.als | 435 ++++++++++++++++++ .../contract/goal/example_scheduling_goal.als | 19 + .../runtime/alloy/lib/data_structure.als | 89 ++++ resources/runtime/alloy/lib/property.als | 37 ++ resources/runtime/alloy/main.als | 25 + resources/runtime/alloy/meta/contract.als | 52 +++ 9 files changed, 675 insertions(+), 1 deletion(-) create mode 100644 resources/runtime/alloy/Makefile.am create mode 100755 resources/runtime/alloy/contract/analysis/example_scheduling_analysis.als create mode 100755 resources/runtime/alloy/contract/goal/example_scheduling_goal.als create mode 100755 resources/runtime/alloy/lib/data_structure.als create mode 100755 resources/runtime/alloy/lib/property.als create mode 100755 resources/runtime/alloy/main.als create mode 100755 resources/runtime/alloy/meta/contract.als diff --git a/configure.ac b/configure.ac index 7cafc51e..904e2a8f 100644 --- a/configure.ac +++ b/configure.ac @@ -419,6 +419,7 @@ AC_OUTPUT([ resources/behavioural_properties/Makefile resources/runtime/Makefile resources/runtime/aadl_xml/Makefile + resources/runtime/alloy/Makefile resources/runtime/cheddar/Makefile resources/runtime/python/Makefile projects/ocarina.gpr diff --git a/resources/runtime/Makefile.am b/resources/runtime/Makefile.am index 752eb3a1..df080948 100644 --- a/resources/runtime/Makefile.am +++ b/resources/runtime/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = cheddar aadl_xml python +SUBDIRS = cheddar aadl_xml python alloy @DEBUG_FALSE@DEBUG_FLAG = --disable-debug @DEBUG_TRUE@DEBUG_FLAG = --enable-debug diff --git a/resources/runtime/alloy/Makefile.am b/resources/runtime/alloy/Makefile.am new file mode 100644 index 00000000..b593817f --- /dev/null +++ b/resources/runtime/alloy/Makefile.am @@ -0,0 +1,16 @@ +AUTOMAKE_OPTIONS = no-dependencies + +BASE_ALLOY_FILES = contract/analysis/example_scheduling_analysis.als \ + contract/goal/example_scheduling_goal.als \ + lib/data_structure.als lib/property.als main.als \ + meta/contract.als + +ALLOY_FILES = $(addprefix $(srcdir)/,$(BASE_ALLOY_FILES)) + +EXTRA_DIST = $(ALLOY_FILES) + +alloy_files = ${shell $(CYGPATH_U) '$(includedir)/ocarina/runtime/alloy'} + +install-data-local: + $(INSTALL) -d $(DESTDIR)$(alloy_files) + for f in $(BASE_ALLOY_FILES); do $(INSTALL) -m 444 -D $(srcdir)/$$f $(DESTDIR)$(alloy_files)/$$f; done diff --git a/resources/runtime/alloy/contract/analysis/example_scheduling_analysis.als b/resources/runtime/alloy/contract/analysis/example_scheduling_analysis.als new file mode 100755 index 00000000..859eb73c --- /dev/null +++ b/resources/runtime/alloy/contract/analysis/example_scheduling_analysis.als @@ -0,0 +1,435 @@ +module contract/analysis/example_scheduling_analysis + +open lib/data_structure + +/********************************************************* + Generated from the repository of analyses +*********************************************************/ + +/* +Declaration of the contracts representing the analyses present in the repository +*/ + +------------------------------- +------- Analyses +------------------------------ + +one sig FPP_RTA extends Contract{ +}{ + assumption= + periodic_tasks + +periodic_tasks_with_jitter + +simultaneous_tasks + +tasks_with_implicit_deadlines + +tasks_with_arbitrary_deadlines + +tasks_with_fixed_priority + +independent_tasks + +tasks_with_bounded_execution_times + +preemtible_tasks + +uniprocessor_architectures + input={S:Component | S.type=system and + (some sub:S.subcomponents | sub.type =processor and + (scheduling_protocol+preemptive_scheduler) in sub.properties) and + (some sub:S.subcomponents | sub.type =process and + thread in sub.subcomponents.type and + ( let th=sub.subcomponents & thread.~type | + (dispatch_protocol +period +compute_execution_time +priority) in th.properties and + (not (deadline) in th.properties and not (offset) in th.properties) + ) + ) + } + guarantee=none + output={/*sys:Component | sys.type=system and + sys.properties=none and + sys.subcomponents={procss:Component | + procss.type=process and + procss.properties=none and + procss.subcomponents={*/ thrd:Component| + thrd.type=thread and + thrd.subcomponents=none and + thrd.properties=response_time + //} + //} + } +} + +one sig pseudo_model1 extends Component{}{ + type=thread + subcomponents=none + properties=response_time +} + +one sig pseudo_model2 extends Component{}{ + type=virtual_bus + subcomponents=none + properties=response_time +} + +one sig pseudo_model3 extends Component{}{ + type=bus + subcomponents=none + properties=response_time +} + +/* +one sig module1 extends Component{}{ + type=system + subcomponents=module1_m1_process + properties=none +} + +one sig module1_m1_process extends Component{}{ + type=process + subcomponents=module1_m1_process_t1 + properties=none +} + +one sig module1_m1_process_t1 extends Component{}{ + type=thread + subcomponents=none + properties=response_time +}*/ + +one sig DC_FPP_RTA extends Contract{ +}{ + assumption= + periodic_tasks + +periodic_tasks_with_jitter + +simultaneous_tasks + +tasks_with_implicit_deadlines + +tasks_with_arbitrary_deadlines + +tasks_with_fixed_priority + +independent_tasks + +tasks_with_bounded_execution_times + +preemtible_tasks + +uniprocessor_architectures + input={S:Component | S.type=system and + (some sub:S.subcomponents | sub.type =processor and + (scheduling_protocol+preemptive_scheduler) in sub.properties) and + (some sub:S.subcomponents | sub.type =process and + thread in sub.subcomponents.type and + ( let th=sub.subcomponents & thread.~type | + (dispatch_protocol +period +compute_execution_time +priority+deadline) in th.properties and + (not (offset) in th.properties) + ) + ) + } + guarantee=none + output={/*sys:Component | sys.type=system and + sys.properties=none and + sys.subcomponents={procss:Component | + procss.type=process and + procss.properties=none and + procss.subcomponents={*/ thrd:Component| + thrd.type=thread and + thrd.subcomponents=none and + thrd.properties=response_time + //} + //} + } + +} + +one sig AD_FPP_RTA extends Contract{}{ + assumption= + periodic_tasks + +periodic_tasks_with_jitter + +simultaneous_tasks + +tasks_with_implicit_deadlines + +tasks_with_arbitrary_deadlines + +tasks_with_fixed_priority + +independent_tasks + +tasks_with_bounded_execution_times + +preemtible_tasks + +uniprocessor_architectures + input={S:Component | S.type=system and + (some sub:S.subcomponents | sub.type =processor and + (scheduling_protocol+preemptive_scheduler) in sub.properties) and + (some sub:S.subcomponents | sub.type =process and + thread in sub.subcomponents.type and + ( let th=sub.subcomponents & thread.~type | + (dispatch_protocol +period +compute_execution_time +priority+deadline) in th.properties and + (not (offset) in th.properties) + ) + ) + } + guarantee=none + output={/*sys:Component | sys.type=system and + sys.properties=none and + sys.subcomponents={procss:Component | + procss.type=process and + procss.properties=none and + procss.subcomponents={*/ thrd:Component| + thrd.type=thread and + thrd.subcomponents=none and + thrd.properties=response_time + //} + //} + } +} + +one sig O_FPP_RTA extends Contract{ +}{ + assumption= + periodic_tasks + +periodic_tasks_with_jitter + +simultaneous_tasks + +tasks_with_implicit_deadlines + +tasks_with_arbitrary_deadlines + +tasks_with_fixed_priority + +independent_tasks + +tasks_with_bounded_execution_times + +preemtible_tasks + +uniprocessor_architectures + input={S:Component | S.type=system and + (some sub:S.subcomponents | sub.type =processor and + (scheduling_protocol+preemptive_scheduler) in sub.properties) and + (some sub:S.subcomponents | sub.type =process and + thread in sub.subcomponents.type and + ( let th=sub.subcomponents & thread.~type | + (dispatch_protocol +period +compute_execution_time +priority+deadline+offset) in th.properties + ) + ) + } + guarantee=none + output={/*sys:Component | sys.type=system and + sys.properties=none and + sys.subcomponents={procss:Component | + procss.type=process and + procss.properties=none and + procss.subcomponents={*/ thrd:Component| + thrd.type=thread and + thrd.subcomponents=none and + thrd.properties=response_time + //} + //} + } +} + +one sig FEASIBILITY_ANALYSIS extends Contract{ +}{ + assumption= + periodic_tasks + +periodic_tasks_with_jitter + +simultaneous_tasks + +tasks_with_implicit_deadlines + +tasks_with_arbitrary_deadlines + +tasks_with_fixed_priority + +independent_tasks + +tasks_with_bounded_execution_times + +preemtible_tasks + +uniprocessor_architectures + input={S:Component | S.type=system and + (some sub:S.subcomponents | sub.type =processor and + (scheduling_protocol+preemptive_scheduler) in sub.properties) and + (some sub:S.subcomponents | sub.type =process and + thread in sub.subcomponents.type and + ( let th=sub.subcomponents & thread.~type | + (dispatch_protocol +period +compute_execution_time +priority+deadline) in th.properties and + (not (offset) in th.properties) + ) + ) + } + guarantee=is_schedulable + output=none +} + +one sig ARINC653_RTA extends Contract {}{ + assumption=arinc653_context + input={S:Component | S.type=system and + (some sub:S.subcomponents | sub.type =processor and + (arinc653__slots_allocation+arinc653__partition_slots+arinc653__module_major_frame) in sub.properties and + virtual_processor in sub.subcomponents.type and + ( let vp=sub.subcomponents & virtual_processor.~type | + (scheduling_protocol) in vp.properties + ) + ) and + (some sub:S.subcomponents | sub.type =process) + } + guarantee=none + output={/*sys:Component | sys.type=system and + sys.properties=none and + sys.subcomponents={procss:Component | + procss.type=process and + procss.properties=none and + procss.subcomponents={*/ thrd:Component| + thrd.type=thread and + thrd.subcomponents=none and + thrd.properties=response_time + //} + //} + } +} + +one sig AFDX_NET_RTA extends Contract{ +}{ + assumption= + periodic_frames+ + periodic_frames_with_jitter+ + simultaneous_fames+ + frames_with_fixed_priority+ + point_to_point_physical_connections+ + messages_with_bounded_size+ + asynchronous_nodes+ + full_duplex_links+ + static_routing + input={S:Component | S.type=system and + (some sub:S.subcomponents | sub.type =system and + (afdx_properties__afdx_es_delay) in sub.properties) and + (some sub:S.subcomponents | sub.type =device and + (afdx_properties__afdx_sw_delay) in sub.properties) and + (some sub:S.subcomponents | sub.type =bus and + (bus_properties__bandwidth) in sub.properties and + virtual_bus in sub.subcomponents.type and + (let vl=sub.subcomponents & virtual_bus.~type | + (afdx_properties__afdx_tx_jitter+afdx_properties__afdx_bandwidth_allocation_gap+afdx_properties__afdx_frame_size) in vl.properties + ) + ) + } + guarantee=none + output= { vl:Component| + vl.type=virtual_bus and + vl.subcomponents=none and + vl.properties=response_time + } +} + +one sig CAN_NET_RTA extends Contract{ +}{ + assumption= + can_context + input={S:Component | S.type=system and + (some sub:S.subcomponents | sub.type =bus and + (bus_properties__available_bandwidth) in sub.properties and + sub.subcomponents.type=none + ) + } + guarantee=none + output= { b:Component| + b.type=bus and + b.subcomponents=none and + b.properties=response_time + } +} + +---------------------------------------- +----- Meta-properties Analyses +---------------------------------------- + +one sig FPP_RTA_META extends Contract{ +}{ + assumption=none + input={thrd:Component | thrd.type=thread and (some p:thrd.properties | p=response_time)} + guarantee=is_schedulable + output=none +} + +one sig AFDX_NET_RTA_META extends Contract{ +}{ + assumption=none + input={vl:Component | vl.type=virtual_bus and (some p:vl.properties | p=response_time)} + guarantee=is_schedulable + output=none +} + +one sig CAN_NET_RTA_META extends Contract{ +}{ + assumption=none + input={b:Component | b.type=bus and (some p:b.properties | p=response_time)} + guarantee=is_schedulable + output=none +} + +---------------------------------------- +----- Contexts Analyses +---------------------------------------- + +one sig LL_context_analysis extends Contract{ +}{ + assumption= none + input={S:Component | S.type=system and + (some sub:S.subcomponents | sub.type =processor and + (scheduling_protocol+preemptive_scheduler) in sub.properties) and + (some sub:S.subcomponents | sub.type =process and + thread in sub.subcomponents.type and + ( let th=sub.subcomponents & thread.~type | + (dispatch_protocol +period +compute_execution_time +priority) in th.properties + ) + ) + } + /* input.type=system + input.subcomponents.type=thread + input.subcomponents.properties=period+execution_time+priority + #input=1*/ + guarantee= + periodic_tasks + +periodic_tasks_with_jitter + +simultaneous_tasks + +tasks_with_implicit_deadlines + +tasks_with_arbitrary_deadlines + +tasks_with_fixed_priority + +independent_tasks + +tasks_with_bounded_execution_times + +preemtible_tasks + +uniprocessor_architectures + output=none +} + +one sig ARINC653_context_analysis extends Contract{ +}{ + assumption= none + input={S:Component | S.type=system and + (some sub:S.subcomponents | sub.type =processor and + (arinc653__slots_allocation+arinc653__partition_slots+arinc653__module_major_frame) in sub.properties and + virtual_processor in sub.subcomponents.type and + ( let vp=sub.subcomponents & virtual_processor.~type | + (scheduling_protocol) in vp.properties + ) + ) and + (some sub:S.subcomponents | sub.type =process) + } + guarantee=arinc653_context + output=none +} + +one sig AFDX_context_analysis extends Contract{ +}{ + assumption= none + input={S:Component | S.type=system and + (some sub:S.subcomponents | sub.type =system and + (afdx_properties__afdx_es_delay) in sub.properties) and + (some sub:S.subcomponents | sub.type =device and + (afdx_properties__afdx_sw_delay) in sub.properties) and + (some sub:S.subcomponents | sub.type =bus and + (bus_properties__bandwidth) in sub.properties and + virtual_bus in sub.subcomponents.type and + (let vl=sub.subcomponents & virtual_bus.~type | + (afdx_properties__afdx_tx_jitter+afdx_properties__afdx_bandwidth_allocation_gap+afdx_properties__afdx_frame_size) in vl.properties + ) + ) + } + guarantee= + periodic_frames+ + periodic_frames_with_jitter+ + simultaneous_fames+ + frames_with_fixed_priority+ + point_to_point_physical_connections+ + messages_with_bounded_size+ + asynchronous_nodes+ + full_duplex_links+ + static_routing + output=none +} + +one sig CAN_context_analysis extends Contract{ +}{ + assumption= none + input={S:Component | S.type=system and + (some sub:S.subcomponents | sub.type =bus and + (bus_properties__available_bandwidth) in sub.properties and + sub.subcomponents.type=none + ) + } + guarantee=can_context + output=none +} diff --git a/resources/runtime/alloy/contract/goal/example_scheduling_goal.als b/resources/runtime/alloy/contract/goal/example_scheduling_goal.als new file mode 100755 index 00000000..1c3f21af --- /dev/null +++ b/resources/runtime/alloy/contract/goal/example_scheduling_goal.als @@ -0,0 +1,19 @@ +module contract/goal/example_scheduling_goal + +open lib/data_structure + +/********************************************************* + Generated from the objective(s) specification +*********************************************************/ + +/* +Declaration of the contract(s) representing the objective(s) +*/ + +one sig is_schedulable extends Contract{ +}{ + assumption= is_schedulable + input=none + guarantee= none + output=none +} diff --git a/resources/runtime/alloy/lib/data_structure.als b/resources/runtime/alloy/lib/data_structure.als new file mode 100755 index 00000000..49076648 --- /dev/null +++ b/resources/runtime/alloy/lib/data_structure.als @@ -0,0 +1,89 @@ +module lib/data_structure + +open lib/property + +/* +Library of Data Structures that can be analyzed +*/ + +//Components +one sig system, device, + process, thread, data, + bus, data_flow, + virtual_bus, virtual_processor, + processor, memory extends Data_Structure{ +} + +//Thread/Tasks properties +one sig dispatch_protocol, + period, + compute_execution_time, + offset, + priority, + deadline, + jitter, + policy, +//processing/scheduling properties + processor_properties__max_prio_first, + preemptive_scheduler, + scheduling_protocol, +//Dataflows properties + afdx_properties__afdx_bandwidth_allocation_gap, //period + afdx_properties__afdx_frame_size, //max_frame_size +// jitter, +//Networking properties + afdx_properties__afdx_tx_jitter, //TxJitterTime + afdx_properties__afdx_es_delay, //TxLatencyTime, RxLatencyTime, + afdx_properties__afdx_sw_delay, //SwLatencyTime, + bus_properties__bandwidth, //speed + bus_properties__available_bandwidth, //speed + bus_properties__channel_type +extends Data_Structure{ +} + +one sig +actual_connection_binding, +actual_memory_binding, +actual_processor_binding, +source_text, +//ARINC 653 properties +arinc653__access_type, +//Deployment properties +deployment__execution_platform +extends Data_Structure{ +} + +//satellite +one sig +source_data_size +extends Data_Structure{ +} + +//mars_pathinder +one sig +posix_scheduling_policy, +concurrency_control_protocol, +data_sheet__uuid +extends Data_Structure{ +} + +//ravenscar +one sig +deployment__process_id, +deployment__channel_address, +compute_entrypoint_source_text, +priority_range, +clock_period +extends Data_Structure{ +} + +//fms +one sig +arinc653__slots_allocation, +arinc653__partition_slots, +arinc653__module_major_frame +extends Data_Structure{ +} + +one sig response_time extends Data_Structure{} + diff --git a/resources/runtime/alloy/lib/property.als b/resources/runtime/alloy/lib/property.als new file mode 100755 index 00000000..73829041 --- /dev/null +++ b/resources/runtime/alloy/lib/property.als @@ -0,0 +1,37 @@ +module lib/property + +open meta/contract + +/* +Library of Properties that can be analyzed +*/ + +one sig uniprocessor_architectures extends Property{ +} + +one sig periodic_tasks, + periodic_tasks_with_jitter, + simultaneous_tasks, + tasks_with_implicit_deadlines, + tasks_with_arbitrary_deadlines, + tasks_with_fixed_priority, + independent_tasks, + tasks_with_bounded_execution_times, + preemtible_tasks extends Property{ +} + +one sig periodic_frames, + periodic_frames_with_jitter, + simultaneous_fames, + frames_with_fixed_priority, + point_to_point_physical_connections, + messages_with_bounded_size, + asynchronous_nodes, + full_duplex_links, + static_routing extends Property{ +} + +one sig is_schedulable extends Property{ +} + +one sig arinc653_context, can_context extends Property{} diff --git a/resources/runtime/alloy/main.als b/resources/runtime/alloy/main.als new file mode 100755 index 00000000..de3c2fec --- /dev/null +++ b/resources/runtime/alloy/main.als @@ -0,0 +1,25 @@ +module main + +open contract/analysis/example_scheduling_analysis +open contract/goal/example_scheduling_goal + +/* +open contract/model/ravenscar_aadl +open contract/model/dre_aadl +open contract/model/pathfinder_aadl +open contract/model/satellite_aadl +open contract/model/fms_aadl +*/ +open con_model + +/* +This is the main alloy file to execute with Alloy Analyzer +Default settings for the Alloy analyzer to be adjusted if necessary +*/ + +fact no_univ_signature{ + Univ=none +} + +//adjust resolution scope if necessary +run {} for 1 diff --git a/resources/runtime/alloy/meta/contract.als b/resources/runtime/alloy/meta/contract.als new file mode 100755 index 00000000..09a32447 --- /dev/null +++ b/resources/runtime/alloy/meta/contract.als @@ -0,0 +1,52 @@ +module meta/contract + +/********************************************************* + + Alloy module +*********************************************************/ + +/*Basic structures manipulated in the Alloy specification*/ + +/*Relationships with Data and Properties can be specified in a contract*/ +abstract sig Data_Structure {} +abstract sig Component { + subcomponents: set Component, + type: lone Data_Structure, + properties: set Data_Structure +} +abstract sig Property {} + +/*Definition of the structure of a contract*/ +abstract sig Contract{ + input: set Component, //required-provided data + output:set Component, + assumption: set Property, //required-provided properties + guarantee: set Property, + // inter-dependencies with other contracts + nextHoriz:set Contract, // output->input + nextVertical:set Contract // guarantee->assumption +} + +/* +Constraints to be held by satisfiable instance(s) +*/ + +//Fact defining an horizontal precedence between two elements +fact HorizontalPrecedence{ + all c_current:Contract | + c_current.nextHoriz={c_next:Contract| + (c_current.output & c_next.input != none) and + (all a :c_current.assumption| a in Contract.guarantee) and + (all a :c_next.assumption| a in Contract.guarantee) //and +// c_current.output != none + } +} + + +//Fact defining a vertical precedence between two elements +fact VerticalPrecedence{ + all c_current:Contract | + c_current.nextVertical={c_next:Contract| + (c_current.guarantee & c_next.assumption != none) + } +} -- GitLab