{"id":"W2148571320","doi":"10.1145/1368088.1368187","title":"Experience applying the SPIN model checker to an industrial telecommunications system","year":2008,"lang":"en","type":"article","venue":"","topic":"Software Reliability and Analysis Research","field":"Computer Science","cited_by":13,"is_retracted":false,"has_abstract":true,"ca_institutions":"Queen's University","funders":"","keywords":"Computer science; Model checking; Telecommunications; Programming language","routes":{"ca_aff":true,"ca_fund":false,"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.007179839,0.0006036286,0.0006304237,0.0006601762,0.001391179,0.001742011,0.001740846,0.001352926,0.002501138],"category_scores_gemma":[0.01877407,0.000435168,0.0005796255,0.0009873069,0.001957374,0.002124512,0.001664037,0.00215963,0.000374247],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001397678,"about_ca_system_score_gemma":0.00189034,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.01183348,"about_ca_topic_score_gemma":0.01224035,"domain_scores_codex":[0.9943694,0.002862368,0.0002533758,0.0003732179,0.00175105,0.0003905019],"domain_scores_gemma":[0.9870749,0.008033533,0.0003361562,0.002148885,0.002032758,0.0003738698],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.001710136,0.004462275,0.04879976,0.001100234,0.0004484238,0.008340607,0.03299472,0.2318576,0.1128878,0.03130259,0.01725394,0.508842],"study_design_scores_gemma":[0.0005404383,0.0041752,0.01180942,0.0002352411,0.0005439559,0.002683992,0.006431683,0.7279256,0.17501,0.0148964,0.0555023,0.0002457135],"study_design_candidate":"bench_or_experimental","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.8737898,0.0003614639,0.1060087,0.001521031,0.0001030102,0.0001748247,0.0001255355,0.002668369,0.01524718],"genre_scores_gemma":[0.9451512,0.0003663073,0.0501733,0.0002449923,0.00002471025,0.00003235241,0.0001517924,0.0003372813,0.003518106],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.01183348,"threshold_uncertainty_score":0.03797108,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1582739223373429,"score_gpt":0.3484139023140468,"score_spread":0.1901399799767039,"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."}}