{"id":"W2542390625","doi":"10.1109/icm.2011.6177381","title":"Formal verification of Time-Triggered Ethernet protocol using PRISM model checker","year":2011,"lang":"en","type":"article","venue":"","topic":"Network Time Synchronization Technologies","field":"Computer Science","cited_by":4,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"Computer science; Ethernet; Model checking; Ethernet over SDH; Protocol (science); Ethernet flow control; ATA over Ethernet; Network interface controller; Embedded system; Prism; State (computer science); Synchronous Ethernet; Computer network; Real-time computing; Algorithm","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.0002136753,0.00009673107,0.0001159503,0.00009296396,0.00004686988,0.00002123973,0.0006933237,0.0001061679,0.0001074886],"category_scores_gemma":[0.00001623188,0.00008301558,0.00003235531,0.0003554384,0.00006217924,0.0006907286,0.0002333317,0.00007003175,0.00006286036],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0000366909,"about_ca_system_score_gemma":0.00009125559,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001752425,"about_ca_topic_score_gemma":4.244877e-7,"domain_scores_codex":[0.9991347,0.00002183757,0.0002652155,0.0002144306,0.0001679687,0.0001958105],"domain_scores_gemma":[0.9991143,0.000005734576,0.0001822784,0.0005829446,0.00008934474,0.00002536115],"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.0001095584,0.0008599033,0.001133309,0.0001921799,0.0001175665,0.000004202521,0.005333715,0.02579966,0.05772148,0.649204,0.005191699,0.2543328],"study_design_scores_gemma":[0.000192243,0.00003343655,0.00007608447,0.000008155183,0.000001722549,0.000001747266,0.000004672802,0.8739604,0.1206309,0.004855705,0.0001437893,0.00009111682],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.001798046,0.000002782277,0.978438,0.00001492345,0.00001462965,0.01058231,2.99053e-7,0.0004242134,0.008724855],"genre_scores_gemma":[0.07307945,5.986889e-7,0.9218022,0.00002677336,0.000009694223,0.004077502,0.000001008661,0.00001211959,0.0009906348],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.8481607,"threshold_uncertainty_score":0.3385277,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05685267992419361,"score_gpt":0.2655586429910484,"score_spread":0.2087059630668548,"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."}}