{"id":"W2109666882","doi":"10.1109/ismvl.2015.17","title":"Using SPIN to Check Nondeterministic Simulink Stateflow Models","year":2015,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Victoria","funders":"Natural Sciences and Engineering Research Council of Canada; Ministry of Education, Culture, Sports, Science and Technology; CMC Microsystems","keywords":"Stateflow; Model checking; Computer science; Promela; Nondeterministic algorithm; Finite-state machine; Abstraction; Programming language; Markov chain; State (computer science); Theoretical computer science; Computer engineering; Machine learning; MATLAB","routes":{"ca_aff":true,"ca_fund":true,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0006196042,0.0001057886,0.0001174639,0.00009297951,0.00004699348,0.0001333341,0.000715546,0.00004457408,0.00000652044],"category_scores_gemma":[0.0001499093,0.00009727228,0.00002519085,0.0003520032,0.00001969903,0.00075428,0.0002608955,0.0000699797,0.000167383],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00009981201,"about_ca_system_score_gemma":0.000132037,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00003776266,"about_ca_topic_score_gemma":0.000001616145,"domain_scores_codex":[0.9988832,0.00006648563,0.0002216632,0.0003033656,0.0002794247,0.0002458123],"domain_scores_gemma":[0.9989028,0.00002715688,0.00005123395,0.0006344665,0.0001432924,0.0002410796],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0000251494,0.00008873414,0.00004944772,0.00002266671,0.00001061203,0.00001978831,0.004683673,0.6924617,0.003544901,0.208209,0.000758386,0.09012599],"study_design_scores_gemma":[0.0001233239,0.00008545822,0.00002885819,0.000006865527,0.000002056872,0.000007935078,0.00003061592,0.9807804,0.003824202,0.01404413,0.0009231306,0.0001429838],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01825943,0.000007398276,0.9716662,0.0001358575,0.000478268,0.000159,9.163286e-7,0.0001724595,0.009120511],"genre_scores_gemma":[0.3172157,3.377282e-7,0.6820945,0.0003887827,0.00003440823,0.000004465388,3.665528e-7,0.000006269089,0.0002552036],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.2989563,"threshold_uncertainty_score":0.3966648,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.3645345270938173,"score_gpt":0.4262703106787759,"score_spread":0.06173578358495857,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}