{"id":"W2161320179","doi":"10.1109/iccd.1998.727045","title":"Model checking of a real ATM switch","year":2002,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":10,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université de Montréal; Concordia University","funders":"Scheme for Promotion of Academic and Research Collaboration","keywords":"Computer science; FIFO (computing and electronics); Asynchronous Transfer Mode; Model checking; Asynchronous communication; Abstraction; Network switch; State (computer science); Embedded system; Transfer (computing); State space; Parallel computing; Computer hardware; Computer network; 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.001197322,0.0004787016,0.0003576858,0.0002864209,0.0005684415,0.0009222096,0.0008759137,0.0006799994,0.002171277],"category_scores_gemma":[0.002362538,0.0002564273,0.0007166065,0.0002467028,0.001068507,0.0009111232,0.0005510529,0.0006224138,0.0001542788],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001193956,"about_ca_system_score_gemma":0.00132978,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.006721875,"about_ca_topic_score_gemma":0.00421724,"domain_scores_codex":[0.9989716,0.0004285349,0.00003646373,0.0001644935,0.0003031762,0.0000957838],"domain_scores_gemma":[0.9989631,0.0007114384,0.00007226646,0.0001265718,0.00009710502,0.00002947327],"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.0005120669,0.0001562023,0.004128376,0.0002859999,0.00009799249,0.0008284203,0.0005045975,0.8437917,0.08794162,0.03445667,0.0008091154,0.02648714],"study_design_scores_gemma":[0.00009031269,0.0002053737,0.0005240946,0.00001441907,0.0000356226,0.0001059587,0.00005367194,0.9525197,0.03765767,0.006638015,0.002142577,0.00001276441],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.6366144,0.0001941087,0.3558498,0.0002184752,0.00004229941,0.00008075204,0.0002165205,0.002320274,0.004463339],"genre_scores_gemma":[0.9523342,0.00006098123,0.04588904,0.0000327664,0.000007902919,0.00003932629,0.0001388699,0.00005491476,0.001441929],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.006721875,"threshold_uncertainty_score":0.01336551,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1128650639139806,"score_gpt":0.3078055524670696,"score_spread":0.194940488553089,"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."}}