Resolute Error in evaluating prove statement

[dpgluch]

comments and screen capture for the error.docx test case.txt

OSATE Version: 2.3.3-SNAPSHOT -- Build id: 2018-03-06

[reteprelief]

Hi Dave, BasicTestCase.txt

Here is the issue. Resolute works on the instance model. Connection instances do not have a simple name or inherit the name from a connection declaration. Instead you can get hold of all connections or connections going in or out of a component.

In the prove statement you can use this or this.subcomponent but not this.conn or this.feature

Attached is some sample resolute: one prints out all connections in the instance model. The other checks encryption on all connections from component one. You could also get the connections for a specific feature (see encryptionForSourceFeature.

Peter

[dpgluch]

Peter,

OK, thanks. I did not think that about connections names in the instance model but it makes sense.

There were no email attachments. Are they on github?

Dave

From: Peter Feiler [mailto:notifications@github.com] Sent: Tuesday, April 03, 2018 10:51 AM To: osate/osate2-core osate2-core@noreply.github.com Cc: David Gluch dpg@sei.cmu.edu; Author author@noreply.github.com Subject: Re: [osate/osate2-core] Resolute Error in evaluating prove statement (#1113)

Hi Dave, BasicTestCase.txthttps://github.com/osate/osate2-core/files/1872013/BasicTestCase.txt

Here is the issue. Resolute works on the instance model. Connection instances do not have a simple name or inherit the name from a connection declaration. Instead you can get hold of all connections or connections going in or out of a component.

In the prove statement you can use this or this.subcomponent but not this.conn or this.feature

Attached is some sample resolute: one prints out all connections in the instance model. The other checks encryption on all connections from component one. You could also get the connections for a specific feature (see encryptionForSourceFeature.

Peter

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHubhttps://github.com/osate/osate2-core/issues/1113#issuecomment-378277831, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AXaqZrcaWDhOlsyALazsCKq3vkyTWc26ks5tk4xigaJpZM4TFKvP.

[reteprelief]

It was attached as an aadl file. Here is its content. I also attached the file to the github issue entry.

Peter

package basic_test_case public

          with Security_Properties;

system basic

end basic;

system implementation basic.one

          subcomponents
                       one: system one;
                       two: system two;

          connections
                       c1: port one.outP1 -> two.inP1 {Security_Properties::encryption=>true;};

          properties
                       Security_Properties::encryption=>true applies to c1;
                        Security_Properties::Information_Security_Level_US => secret;

annex resolute {**

          prove print_connections(this)
          prove encryptionForSource(this.one)
          prove has_secret_information_level_security (this)

-- encryption is defined in Security_Properties as

-- encryption: aadlboolean applies to (all);

**};

--

end basic.one;

system one features outP1: out data port;

          properties
                       Period => 20ms;
                        Security_Properties::Information_Security_Level_US => Top_Secret;

end one;

system two features inP1: in data port; end two;

annex resolute { print_connections (c: component) <= "prints connections for component " c ** forall (conn: connection). printconn(conn)

                       printconn(conn:connection) <= ** conn ** true

                       encryptionForSource(src: component) <=
                       ** "encryption for all outgoing connections" **
                       forall (conn: connections(src)) . has_encryption(conn)

                       encryptionForSourceFeature(src: component) <=
                       ** "encryption for all outgoing connections" **
                       let one :  {feature} = {f for (f:features(src))| name(f) = "outP1"};
                       forall (outp: one).
                       forall (conn: connections(outp)) . has_encryption(conn)

                       has_encryption (conn: connection) <=
                       ** "checks that the encryption property is assigned a value for the connection." **
                       has_property (conn, Security_Properties::encryption)

                       has_secret_information_level_security (c: component) <=
                       ** "checks that the information security level property is assigned a value for the component." **
                       has_property (c, Security_Properties::Information_Security_Level_US)

**};

end basic_test_case;

From: dpgluch [mailto:notifications@github.com] Sent: Tuesday, April 3, 2018 2:54 PM To: osate/osate2-core osate2-core@noreply.github.com Cc: Peter Feiler phf@sei.cmu.edu; Comment comment@noreply.github.com Subject: Re: [osate/osate2-core] Resolute Error in evaluating prove statement (#1113)

Peter,

OK, thanks. I did not think that about connections names in the instance model but it makes sense.

There were no email attachments. Are they on github?

Dave

From: Peter Feiler [mailto:notifications@github.com] Sent: Tuesday, April 03, 2018 10:51 AM To: osate/osate2-core osate2-core@noreply.github.com<mailto:osate2-core@noreply.github.com> Cc: David Gluch dpg@sei.cmu.edu<mailto:dpg@sei.cmu.edu>; Author author@noreply.github.com<mailto:author@noreply.github.com> Subject: Re: [osate/osate2-core] Resolute Error in evaluating prove statement (#1113)

Hi Dave, BasicTestCase.txthttps://github.com/osate/osate2-core/files/1872013/BasicTestCase.txt

Here is the issue. Resolute works on the instance model. Connection instances do not have a simple name or inherit the name from a connection declaration. Instead you can get hold of all connections or connections going in or out of a component.

In the prove statement you can use this or this.subcomponent but not this.conn or this.feature

Attached is some sample resolute: one prints out all connections in the instance model. The other checks encryption on all connections from component one. You could also get the connections for a specific feature (see encryptionForSourceFeature.

Peter

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHubhttps://github.com/osate/osate2-core/issues/1113#issuecomment-378277831, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AXaqZrcaWDhOlsyALazsCKq3vkyTWc26ks5tk4xigaJpZM4TFKvP.

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://github.com/osate/osate2-core/issues/1113#issuecomment-378358220, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AAtzuKhobQoCZ4tiKwOlKoT17hsHDNFHks5tk8VFgaJpZM4TFKvP.

[reteprelief]

I will add an issue enhancement for ALISA to support proof calls on items other than component instances. See osate/osate2-core#1147