{"id":"W1812469182","doi":"","title":"Verifying protocols by model checking: a case study of the wireless application protocol and the model checker SPIN","year":2004,"lang":"en","type":"article","venue":"Conference of the Centre for Advanced Studies on Collaborative Research","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":7,"is_retracted":false,"has_abstract":true,"ca_institutions":"McMaster University","funders":"","keywords":"Model checking; Computer science; Protocol (science); Promela; Formal verification; Wireless; Wireless Application Protocol; Database transaction; Formal methods; Distributed computing; Programming language; Wireless network; Operating system","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.01172319,0.0008448424,0.0008971667,0.0009866359,0.002251121,0.002494825,0.001764595,0.003418481,0.001393571],"category_scores_gemma":[0.02733124,0.0007497072,0.001178639,0.001577957,0.004971195,0.004803288,0.002455916,0.003547971,0.0001578745],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001529434,"about_ca_system_score_gemma":0.002530607,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.01147423,"about_ca_topic_score_gemma":0.01063233,"domain_scores_codex":[0.9881105,0.006368101,0.0004664697,0.0005794758,0.003754044,0.0007213774],"domain_scores_gemma":[0.9629508,0.03090487,0.001073468,0.003434669,0.001321694,0.000314542],"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.001438904,0.001260544,0.01436905,0.001187444,0.0003246776,0.01326329,0.01201333,0.4159392,0.03301742,0.3792282,0.004323685,0.1236342],"study_design_scores_gemma":[0.0003988688,0.0007226067,0.001564426,0.0001992926,0.0002494581,0.003281359,0.00228353,0.8303241,0.06184304,0.08156253,0.01746023,0.0001106676],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"empirical","genre_gemma":"methods","genre_scores_codex":[0.5711381,0.001181986,0.4072203,0.003100403,0.00008210704,0.0004901818,0.0001415029,0.001838556,0.01480691],"genre_scores_gemma":[0.869045,0.0005206085,0.1269798,0.0001640478,0.00002746523,0.0001571977,0.00009618312,0.0002513053,0.002758458],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.01172319,"threshold_uncertainty_score":0.0619989,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.2025073741627581,"score_gpt":0.489088301158166,"score_spread":0.2865809269954079,"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."}}