diff --git a/README.md b/README.md index 425b38c..e7dad6c 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 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 +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: @@ -61,14 +65,20 @@ More information about CoCoSim can be found [here](https://github.com/coco-team/ * Lead Developer: [Temesghen Kahsai](http://www.lememta.info/) -## Current Contributors +* 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 -* [Hamza Bourbouh] (https://hbourbouh.github.io/) -* Pierre-Loic Garoche (Onera - France) -* Claire Pagetti (Onera - France) -* Eric Noulard (Onera - France) -* Thomas Loquen (Onera - France) +CoCoSim is partially funded by: -## Past Contributors + * NASA NRA NNX14AI09G + * NSF award 1136008 -* Arnaud Dieumegard (Fabruary - August 2015) +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. 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; 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