{"id":"W2133953358","doi":"10.1109/icnp.1993.340891","title":"An approach to evaluating the performance of communication protocols based on formal specifications","year":2002,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":4,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Extended finite-state machine; Reachability; Computer science; Finite-state machine; Formal methods; Formal verification; State space; Protocol (science); Queueing theory; Sliding window protocol; State (computer science); Communications protocol; Formal specification; Model checking; Theoretical computer science; Automaton; Simple (philosophy); Window (computing); Programming language; Computer network; Operating system; Mathematics","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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002122502,0.00009159029,0.00009110191,0.00009486356,0.0003066034,0.00008989836,0.001947255,0.00003502821,0.00002477867],"category_scores_gemma":[0.0001041668,0.00006403794,0.00003041386,0.0006128767,0.00005458073,0.0008198548,0.00009390443,0.0001292781,0.00004565447],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00004041253,"about_ca_system_score_gemma":0.00002125147,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000004003592,"about_ca_topic_score_gemma":4.075038e-7,"domain_scores_codex":[0.9985677,0.0003370078,0.0002847048,0.0002216024,0.0004118232,0.0001771848],"domain_scores_gemma":[0.9972005,0.0001149048,0.0001604426,0.0022976,0.0001739183,0.00005261249],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00004293085,0.001016318,0.0006661053,0.00004868198,0.00000574079,2.02466e-8,0.002756834,0.1340139,0.00588417,0.5946526,0.0003897319,0.260523],"study_design_scores_gemma":[0.0001376738,0.0005364538,0.009015985,0.00001931968,0.000001641535,9.762292e-7,0.00004457888,0.9818019,0.007875415,0.00006603137,0.0004163626,0.00008361408],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02209212,0.0000023943,0.9293007,0.0005049111,0.00002309468,0.006416138,9.010334e-7,0.0001009513,0.04155884],"genre_scores_gemma":[0.4554772,6.204787e-7,0.5408164,0.0001774504,0.000009560031,0.003441338,0.000001710719,0.000003897443,0.00007188867],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.847788,"threshold_uncertainty_score":0.3618518,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.3071351936941251,"score_gpt":0.4074903902222816,"score_spread":0.1003551965281564,"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."}}