Commit 57f39581 authored by yoogx's avatar yoogx

* Addition of the Alloy library

        For issue #68
parent d919a2f3
......@@ -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
......
SUBDIRS = cheddar aadl_xml python
SUBDIRS = cheddar aadl_xml python alloy
@DEBUG_FALSE@DEBUG_FLAG = --disable-debug
@DEBUG_TRUE@DEBUG_FLAG = --enable-debug
......
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
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
}
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
}
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{}
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{}
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