{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002050134,0.0008584158,0.0006217326,0.001031141,0.0006052903,0.001265816,0.001181604,0.0006036568,0.002436277],"category_scores_gemma":[0.007731414,0.0005672503,0.001289921,0.0005703779,0.001282347,0.002588456,0.001382468,0.0009915248,0.0002302234],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0008729491,"about_ca_system_score_gemma":0.00215554,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00677599,"about_ca_topic_score_gemma":0.009780703,"domain_scores_codex":[0.9978249,0.0006309761,0.0001881306,0.0003837715,0.0007907363,0.0001813698],"domain_scores_gemma":[0.9933584,0.004071518,0.0006901022,0.001248754,0.0005143225,0.0001168305],"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.0008139479,0.0002358209,0.01225726,0.0006876429,0.0004108156,0.0008653044,0.0004798242,0.7684308,0.04833513,0.09408996,0.001302961,0.0720905],"study_design_scores_gemma":[0.00004842455,0.0001245896,0.0003817255,0.00002997258,0.0000725896,0.00008567529,0.00004320928,0.9247231,0.04845083,0.02385918,0.002149488,0.00003118097],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.09700432,0.00009953458,0.8922888,0.00007934166,0.0000474984,0.00007565118,0.0002639796,0.008475901,0.001664898],"genre_scores_gemma":[0.7371435,0.000121043,0.2601757,0.00006225,0.00001066817,0.0001317716,0.0004821631,0.0004994064,0.001373476],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.00677599,"threshold_uncertainty_score":0.01347309,"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."}}