{"id":"W4255962326","doi":"10.2991/ijndc.2016.4.1.7","title":"Using SPIN to Check Simulink Stateflow Models","year":2016,"lang":"en","type":"article","venue":"The International journal of networked and distributed computing","topic":"Business Process Modeling and Analysis","field":"Business, Management and Accounting","cited_by":1,"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; Computer science; Programming language; Embedded system; Software engineering; 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.0006344041,0.0001662179,0.0002413069,0.0001916179,0.0002073661,0.0004263505,0.0005427282,0.0000451261,0.00001696456],"category_scores_gemma":[0.00006000412,0.00009795801,0.0001231077,0.0003598381,0.00004081568,0.0006094273,0.0002698466,0.0001310404,0.000006942142],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00005628953,"about_ca_system_score_gemma":0.00004098027,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00008595551,"about_ca_topic_score_gemma":0.00001003048,"domain_scores_codex":[0.998533,0.00001334487,0.000541422,0.0001860811,0.000469143,0.000257083],"domain_scores_gemma":[0.9981841,0.00009733818,0.000556131,0.0001077954,0.001018052,0.00003655957],"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.000113089,0.00003913947,0.002077187,0.00001230552,0.0001637392,0.00002502596,0.00003521397,0.9263358,0.0003988303,0.0007831161,0.0008833107,0.06913321],"study_design_scores_gemma":[0.0006947812,0.000007057257,0.000401119,0.0003229713,0.0000849328,0.00002713769,0.00008873412,0.9859425,0.00000769405,0.007419637,0.004844632,0.0001587939],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.2889868,0.0001515451,0.7073138,0.002890201,0.0004806469,0.00003882473,0.000006413654,0.00002336603,0.0001084203],"genre_scores_gemma":[0.9943072,0.00002420858,0.00102847,0.001235634,0.00335578,4.07379e-7,0.000009466791,0.00001666928,0.00002214693],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.7062854,"threshold_uncertainty_score":0.4111308,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0414733582807776,"score_gpt":0.2750858829101968,"score_spread":0.2336125246294192,"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."}}