{"id":"W2240436135","doi":"10.1109/tencon.2015.7373092","title":"SPIN model checking for the BEE system","year":2015,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Victoria","funders":"CMC Microsystems","keywords":"Stateflow; Model checking; Computer science; Nondeterministic algorithm; Spin (aerodynamics); Theoretical computer science; Programming language; MATLAB; Engineering; Mechanical engineering","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.001021739,0.0005118067,0.0007243966,0.0006195525,0.0007103775,0.001473321,0.0007051549,0.0005308859,0.003226141],"category_scores_gemma":[0.003018006,0.0003292305,0.00115041,0.0004214196,0.001289791,0.001429636,0.001143917,0.001072758,0.0002550159],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001124588,"about_ca_system_score_gemma":0.00203826,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.01310237,"about_ca_topic_score_gemma":0.0184852,"domain_scores_codex":[0.9990768,0.0002404442,0.00004557577,0.0001125808,0.0003992444,0.0001252803],"domain_scores_gemma":[0.9984902,0.0008096995,0.0001347167,0.0003380636,0.0001848766,0.00004245975],"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.0003436799,0.0001192171,0.002616601,0.0002565525,0.00009987291,0.0004440043,0.0002718961,0.7063725,0.01592828,0.2294427,0.002294682,0.04181],"study_design_scores_gemma":[0.00004802703,0.0000492523,0.0002110555,0.00002512473,0.00003022776,0.0000398376,0.00003838789,0.9237452,0.00787157,0.0654634,0.002460485,0.00001734315],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.1306493,0.0002954029,0.8492947,0.0003996214,0.0001099156,0.0001199761,0.0003102555,0.004652552,0.01416829],"genre_scores_gemma":[0.9060354,0.0001804904,0.08953682,0.00009934048,0.00001812165,0.0000980974,0.0002951401,0.0002404309,0.003496123],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01310237,"threshold_uncertainty_score":0.02605218,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1606182181921288,"score_gpt":0.3553622359804744,"score_spread":0.1947440177883456,"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."}}