From 655420c492fc7a996e18a41a6d487d9971ada747 Mon Sep 17 00:00:00 2001 From: Teme Date: Fri, 10 Feb 2017 14:57:28 -0800 Subject: [PATCH 1/7] some modifications to the reamde --- README.md | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 53c15ba..e20184e 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,12 @@ # CoCoSim -CoCoSim is an automated analysis framework for Simulink and Stateflow models. CoCoSim is currently under development. We welcome any feedback and bug report. +CoCoSim is an automated analysis and code generatation framework for +Simulink and Stateflow models. Specifically, CoCoSim can be used to +verify automatically user-supplied safety requirements. Moreover, +CoCoSim can be used to generate C and/or Rust code. CoCoSim uses +Lustre as its intermediate language. CoCoSim is currently under +development. We welcome any feedback and bug report. [![ScreenCast of CoCoSim](http://i.imgur.com/itLte0X.png)](https://youtu.be/iqwVCiU46Y4) @@ -12,7 +17,6 @@ The CoCoSim toolbox contains linux and osx binariers for the backend solvers. Download the [CoCoSim ToolBox](https://github.com/coco-team/cocoSim/releases) - ## Installation CoCoSim can be installed and used as follows: @@ -63,7 +67,7 @@ More information about CoCoSim can be found [here](https://github.com/coco-team/ ## Current Contributors -* Hamza Bourbouh +* Hamza Bourbouh (SGT - USA) * Pierre-Loic Garoche (Onera - France) * Claire Pagetti (Onera - France) * Eric Noulard (Onera - France) @@ -72,3 +76,15 @@ More information about CoCoSim can be found [here](https://github.com/coco-team/ ## Past Contributors * Arnaud Dieumegard (Fabruary - August 2015) + + +## Acknowledgments and Disclaimers + +CoCoSim is partially funded by: + + * NASA NRA NNX14AI09G + * NSF award 1136008 + +Any opinions, findings and conclusions or recommendations expressed in +this material are those of the author(s) do not necessarily +reflect the views of NASA and NSF. From 85e112f1caf91a398e468e975ff48db36919178f Mon Sep 17 00:00:00 2001 From: Teme Date: Fri, 10 Feb 2017 15:00:44 -0800 Subject: [PATCH 2/7] some modifications to the reamde --- README.md | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/README.md b/README.md index e20184e..bae1be8 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ # CoCoSim -CoCoSim is an automated analysis and code generatation framework for +CoCoSim is an automated analysis and code generation framework for Simulink and Stateflow models. Specifically, CoCoSim can be used to verify automatically user-supplied safety requirements. Moreover, CoCoSim can be used to generate C and/or Rust code. CoCoSim uses @@ -63,19 +63,17 @@ More information about CoCoSim can be found [here](https://github.com/coco-team/ ## Developers -* Lead Developer: [Temesghen Kahsai](http://www.lememta.info/) - -## Current Contributors - -* Hamza Bourbouh (SGT - USA) -* Pierre-Loic Garoche (Onera - France) -* Claire Pagetti (Onera - France) -* Eric Noulard (Onera - France) -* Thomas Loquen (Onera - France) - -## Past Contributors - -* Arnaud Dieumegard (Fabruary - August 2015) +* Lead Developer: +** [Temesghen Kahsai](http://www.lememta.info/) +* Current Contributors +** Hamza Bourbouh (SGT - USA) +** Pierre-Loic Garoche (Onera - France) +** Claire Pagetti (Onera - France) +** Eric Noulard (Onera - France) +** Thomas Loquen (Onera - France) + +* Past Contributors +** Arnaud Dieumegard (Fabruary - August 2015) ## Acknowledgments and Disclaimers From f65046dc899b4ab5859f29c46c7168e68d20fe99 Mon Sep 17 00:00:00 2001 From: Teme Date: Fri, 10 Feb 2017 15:01:49 -0800 Subject: [PATCH 3/7] some modifications to the reamde --- README.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index bae1be8..c627dc9 100644 --- a/README.md +++ b/README.md @@ -64,16 +64,17 @@ More information about CoCoSim can be found [here](https://github.com/coco-team/ ## Developers * Lead Developer: -** [Temesghen Kahsai](http://www.lememta.info/) +++ [Temesghen Kahsai](http://www.lememta.info/) + * Current Contributors -** Hamza Bourbouh (SGT - USA) -** Pierre-Loic Garoche (Onera - France) -** Claire Pagetti (Onera - France) -** Eric Noulard (Onera - France) -** Thomas Loquen (Onera - France) +++ Hamza Bourbouh (SGT - USA) +++ Pierre-Loic Garoche (Onera - France) +++ Claire Pagetti (Onera - France) +++ Eric Noulard (Onera - France) +++ Thomas Loquen (Onera - France) * Past Contributors -** Arnaud Dieumegard (Fabruary - August 2015) +++ Arnaud Dieumegard (Fabruary - August 2015) ## Acknowledgments and Disclaimers From 10d7c2dd1b91a8942b8bb8b8fe3ac33b1ac88a1b Mon Sep 17 00:00:00 2001 From: Teme Date: Fri, 10 Feb 2017 15:02:38 -0800 Subject: [PATCH 4/7] some modifications to the reamde --- README.md | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/README.md b/README.md index c627dc9..409d15a 100644 --- a/README.md +++ b/README.md @@ -63,18 +63,13 @@ More information about CoCoSim can be found [here](https://github.com/coco-team/ ## Developers -* Lead Developer: -++ [Temesghen Kahsai](http://www.lememta.info/) - -* Current Contributors -++ Hamza Bourbouh (SGT - USA) -++ Pierre-Loic Garoche (Onera - France) -++ Claire Pagetti (Onera - France) -++ Eric Noulard (Onera - France) -++ Thomas Loquen (Onera - France) - -* Past Contributors -++ Arnaud Dieumegard (Fabruary - August 2015) +* Lead Developer: [Temesghen Kahsai](http://www.lememta.info/) + +* Current Contributors: Hamza Bourbouh (SGT - USA), Pierre-Loic + Garoche (Onera - France), Claire Pagetti (Onera - France), Eric + Noulard (Onera - France),Thomas Loquen (Onera - France) + +* Past Contributors: Arnaud Dieumegard (Fabruary - August 2015) ## Acknowledgments and Disclaimers From 2efa9000ebd2098cc28c3c88b5b99da2d4ec0fdb Mon Sep 17 00:00:00 2001 From: Teme Date: Fri, 10 Feb 2017 15:03:35 -0800 Subject: [PATCH 5/7] some modifications to the reamde --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 409d15a..5e65367 100644 --- a/README.md +++ b/README.md @@ -67,7 +67,7 @@ More information about CoCoSim can be found [here](https://github.com/coco-team/ * Current Contributors: Hamza Bourbouh (SGT - USA), Pierre-Loic Garoche (Onera - France), Claire Pagetti (Onera - France), Eric - Noulard (Onera - France),Thomas Loquen (Onera - France) + Noulard (Onera - France), Thomas Loquen (Onera - France) * Past Contributors: Arnaud Dieumegard (Fabruary - August 2015) From de0dfc30547f69184afd97587e3b21f9d832d392 Mon Sep 17 00:00:00 2001 From: Tanja de Jong Date: Thu, 23 Feb 2017 21:26:09 +0100 Subject: [PATCH 6/7] Added function to CoCoSim menu to annotate with CoCoSpec --- sl_customization.m | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/sl_customization.m b/sl_customization.m index 1aa343e..a44fc06 100644 --- a/sl_customization.m +++ b/sl_customization.m @@ -19,9 +19,9 @@ function sl_customization(cm) schema.statustip = 'Automated Analysis Framework'; schema.autoDisableWhen = 'Busy'; - schema.childrenFcns = {@getVerify,@getValidate,... - @getCheckBlocks, @viewContract, @getProps, ... - @getPP, @getCompiler}; + schema.childrenFcns = {@getVerify,@getValidate, ... + @getCheckBlocks, @viewContract, @annotateContract, ... + @getProps, @getPP, @getCompiler}; end function schema = getCheckBlocks(callbackInfo) @@ -143,6 +143,24 @@ function viewContractCallback(callbackInfo) display_msg(ME.getReport(),Constants.DEBUG,'viewContract',''); end end + +% Function to annotate the Simulink model with the generated CoCoSpec +function schema = annotateContract(callbackInfo) + schema = sl_action_schema; + schema.label = 'Annotate with generated CoCoSpec (Experimental)'; + schema.callback = @annotateContractCallback; + end + + function annotateContractCallback(callbackInfo) + try + [prog_path, fname, ext] = fileparts(mfilename('fullpath')); + simulink_name = gcs; + annotate_cocospec(simulink_name); + + catch ME + disp(ME.message) + end + end function schema = getProps(callbackInfo) schema = sl_action_schema; From 1df52db049bba4023199a64a6de7c441e1ab68c8 Mon Sep 17 00:00:00 2001 From: Tanja de Jong Date: Thu, 23 Feb 2017 21:27:10 +0100 Subject: [PATCH 7/7] Added functionality to add a Matlab Function block to a model with the generated CoCoSpec as a comment --- src/annotate_cocospec.m | 86 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) create mode 100644 src/annotate_cocospec.m diff --git a/src/annotate_cocospec.m b/src/annotate_cocospec.m new file mode 100644 index 0000000..3b41d78 --- /dev/null +++ b/src/annotate_cocospec.m @@ -0,0 +1,86 @@ +function insert_embedded( model_full_path ) + % Load the system + open_system(char(model_full_path)); + [model_path, file_name, ext] = fileparts(model_full_path); + lus_path = [fileparts(which(file_name)) '/lustre_files/src_' file_name '/' file_name '.lus.coco']; + + % Create CoCoSpec block + create_cocospec_block(file_name); + + S = sfroot; + B = S.find('Name', 'CoCoSpec', '-isa', 'Stateflow.EMChart'); + + current_code = strread(B.Script, '%s', 'delimiter', sprintf('\n')); + + fid = fopen(lus_path); + + % Add CoCoSpec to code in Matlab function block + code = sprintf([current_code{1} '\n\n']); + while true + line = [fgets(fid)]; + if ~ischar(line); break; end; + code = [code '% ' line]; + end + code = [code sprintf('\n') current_code{numel(current_code)}]; + + % Write code to Matlab function block + B.Script = code; + + fclose(fid); +end + +%% Creates the CoCoSpec block object +function cocospec = create_cocospec_block(file_name) + % Create block + observer_path = [file_name '/CoCoSpec']; + observer = add_block('simulink/User-Defined Functions/MATLAB Function', observer_path); + % Set block position + obs_pos = get_obs_position(file_name); + set_param(observer_path, 'Position', obs_pos); +end + +%% Get the Position value according to the type of block +function[out] = pos(offset_x, offset_y, port_type) +% Block position settings +y = 30; +w = 30; +if strcmp(port_type, 'Inport') + x = 30; + h = 15; +elseif strcmp(port_type, 'Outport') + x = 400; + h = 15; +elseif strcmp(port_type, 'Terminator') + x = 100; + h = 20; + w = 20; +else + x = 30; + h = 30; +end + +offset = 60; +out = [x+offset*offset_x y+offset*offset_y x+offset*offset_x+w y+offset*offset_y+h]; + +end + +%% Returns the Position parameter value for the Observer to be generated +function [obs_pos] = get_obs_position(parent_subsystem) + blocks = find_system(parent_subsystem, 'SearchDepth', 1, 'FindAll', 'on', 'Type', 'Block'); + positions = get_param(blocks, 'Position'); + max_x = 0; + min_x = 0; + max_y = 0; + min_y = 0; + for idx_pos=1:numel(positions) + max_x = max(max_x, positions{idx_pos}(1)); + if idx_pos == 1 + min_x = positions{idx_pos}(1); + min_y = positions{idx_pos}(2); + else + min_x = min(min_x, positions{idx_pos}(1)); + min_y = min(min_y, positions{idx_pos}(2)); + end + end + obs_pos = [max_x max_y (max_x + 150) (max_y + 60)]; +end