osate / examples Goto Github PK

Hi. I'm stating with AADL and OSATE. When I import SafetTutorial example I get errors and warnings
Description Resource Path Location Type
Referenced error propagation flightSurfaceControl must be an in propagation FlightSystem.aadl /SafetyTutorial/packages line: 8 /SafetyTutorial/packages/FlightSystem.aadl Xtext Check (fast)
Referenced error propagation flightSurfaceControl must be an in propagation FlightSystem.aadl /SafetyTutorial/packages line: 9 /SafetyTutorial/packages/FlightSystem.aadl Xtext Check (fast)
Referenced error propagation location must be an in propagation GPSSystem.aadl /SafetyTutorial/packages line: 6 /SafetyTutorial/packages/GPSSystem.aadl Xtext Check (fast)
Referenced error propagation location must be an in propagation GPSSystem.aadl /SafetyTutorial/packages line: 7 /SafetyTutorial/packages/GPSSystem.aadl Xtext Check (fast)
Referenced error propagation location must be an in propagation GPSSystem.aadl /SafetyTutorial/packages line: 7 /SafetyTutorial/packages/GPSSystem.aadl Xtext Check (fast)
Referenced error propagation location must be an in propagation GPSSystem.aadl /SafetyTutorial/packages line: 9 /SafetyTutorial/packages/GPSSystem.aadl Xtext Check (fast)
Referenced error propagation outLocation must be an in propagation GPSSystem.aadl /SafetyTutorial/packages line: 6 /SafetyTutorial/packages/GPSSystem.aadl Xtext Check (fast)

How can i fix it? Thanks!

My osate version is: Version: 2.7.0.vfinal -- Build id: 2020-02-04

Hi,

Can anyone suggest the suitable procedure in developing the plugin of PRISM for OSATE? We are working in Aerospace domain and have lot of AADL Aerospace architecture models that needs to be verified using PRISM.

According to documentation the systems needs at least two operational sensors and at least one operational actuator. The logic implemented says that at least one operational actuator makes the system operational, and at least one failed actuator makes the system failed, so a condition can exist that makes the system operational and failed at the same time. This error also exists in the wiki.sei.cmu.edu page referenced in the model.

[(at least two sensors operational) or (a1.Operational or a2.Operational)]-> Operational;
[a1.Failed or a2.Failed]-> Failed;

Should be:
[(at least two sensors operational) and (a1.Operational or a2.Operational)]-> Operational;
[a1.Failed and a2.Failed]-> Failed;

osate/examples/embedded-control/aadl-model/embedded-control-advanced.aadl lines 283-284
osate/examples/embedded-control/aadl-model/embedded-control.aadl lines 217-218

I am looking into the speed regulation example and generating a Fault Tree
My understanding of redundant components in a fault tree should have an and operator above both.

Is there a way to represent redundant components in AADL so that the fault tree exported is correct?

I have a new download of osate2 2.3.4 on debian 9. The first example I pulled into and AADL project was the embedded controller (as I wanted to play with the prism export). Embedded-control and embedded-control-advance files report errors against s1..s3 and a1..a2, at the ends of the files where the wing values are set. Errors of the form below (subset used to avoid clutter):

Description Resource Path Location Type
Couldn't resolve reference to 's1'. embedded-control-advanced.aadl /embedded-control/aadl-model line: 19 /embedded-control/aadl-model/embedded-control-advanced.aadl Xtext Check (fast)

Description Resource Path Location Type
Couldn't resolve reference to 'Failed'. embedded-control.aadl /embedded-control/aadl-model line: 19 /embedded-control/aadl-model/embedded-control.aadl Xtext Check (fast)

What would I need do to fix this? Is there lib or other file or is this a problem with the example?

Cheers,
A

For integration.software_distributed in examples/latency-case-study/integration.aadl, no report is generated when Check Flow Latency is executed, but a NullPointerException occurs.

This will appear in OSATE version 2.8 and later. I think the reason for the error is that the model is not fully modeled, that is, all flows in the model should be explicitly declared.

We can try to add some code in integration.software_distributed :

system implementation integration.software_distributed extends integration.software_generic
	subcomponents
		s1_cpu 	: processor latency_cs::platform::generic_cpu;
		s2_cpu 	: processor latency_cs::platform::generic_cpu;
		p_cpu 	: processor latency_cs::platform::generic_cpu;
		a_cpu 	: processor latency_cs::platform::generic_cpu;
		s_p_bus: bus latency_cs::platform::generic_bus;
		p_a_bus : bus latency_cs::platform::generic_bus;
	connections
		b0 : bus access s1_cpu.net <-> s_p_bus;
		b1 : bus access s2_cpu.net <-> s_p_bus;
		b2 : bus access p_cpu.net <-> s_p_bus;
		b3 : bus access p_cpu.net <-> p_a_bus;
		b4 : bus access a_cpu.net <-> p_a_bus;
	
	-- to make the model complete, etef2 and etef3 are added here
	flows
		etef2 : end to end flow s1.sensor_source -> c0 -> p.sink0; 
		etef3 : end to end flow s2.sensor_source -> c1 -> p.sink1;
	
	properties
		actual_processor_binding => (reference (s1_cpu)) applies to s1;
		actual_processor_binding => (reference (s2_cpu)) applies to s2;
		actual_processor_binding => (reference (p_cpu)) applies to p;
		actual_processor_binding => (reference (a_cpu)) applies to a;
		
		actual_connection_binding => (reference (s_p_bus)) applies to c0;
		actual_connection_binding => (reference (s_p_bus)) applies to c1;
		actual_connection_binding => (reference (p_a_bus)) applies to c2;
		
		-- protocol that applies to the connections
		required_virtual_bus_class => (classifier (latency_cs::platform::generic_protocol)) applies to c0, c1, c2;
end integration.software_distributed;

I use OSATE2 2.6.1.vfinal.

When testing the examples simple.aadl.
I get issues that say:
"mybus..." must be a port, parameter, data access, feature group, or abstract feature.

I have three questions:

• Is this example "deprecated"?
• Is it my osate2 version that does not work properly?
• Could you correct this example?

Best regards

Hi,

first of all thank you for your help in my previous issue. I have a new problem with the PRISM models generated in OSATE.

When I used the model checker PRISM (version 4.1.beta 2-linux 64) to analyze the models generated in OSATE I found syntactic errors in the generated model ".pm" in some examples. I want to know what version of PRISM I have to use to analyze these PRISM models.

For information, I asked for help in the PRISM forum about the errors in the model example "embedded-control," here is the link of the problem and the solution that was given to me:

https://groups.google.com/forum/?fromgroups #! topic/prismmodelchecker/UmBLG9ur1n0

Best regards,

Smail.

Dear all,

i'm trying to use the Error Model Annex of AADL in osate (osate2-2.0.3) but i have some errors in the following folders ARP4761, error-model and Train. For example in ARP4761>integration>main.aadl i have this error : "mismatched input 'type' expecting 'behavior' ". I have different errors in the other folders. I want to know why I have these errors.

Best regards.

Smail.

As far as I can see Mbytesps used in AppSystems.aadl -> EmbeddedApp.Topology is not a valid unit of SEI::BandWidthBudget.

Hello

For the last couple of days I have been trying to get into AADL and is not going as well as I hoped.
I am trying to use your examples to get started but I am unable to get it up and running.

I watched a video on one of your examples on speed regulation and wanted to try that out first.

I am unable to get anything out of it because of the multiple errors I am getting in the project errors.txt (Please note that this is a html file, please change the extension from txt to html). I have tested a few others and the seem to always get errors.

I followed the instructions online to install osate and currently have version 2.2.1.vupdate01
My java jdk is 1.8.0_101

Here is a example of the environment I am working with

I tried also cloning both osate2-core and osate2-plugins and copied the content to my plug-in folder in the osate2 folder without any changes.

Am i missing some configuration or package to be able to work with this repository?