{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002223974,0.0005639381,0.0005926554,0.000641036,0.000531994,0.001206882,0.001618244,0.0007864551,0.002048705],"category_scores_gemma":[0.005072013,0.0004580172,0.001381499,0.0004445291,0.001136866,0.001417101,0.0010627,0.001568496,0.0002469824],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0008119278,"about_ca_system_score_gemma":0.003625147,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.006325846,"about_ca_topic_score_gemma":0.004420978,"domain_scores_codex":[0.9978468,0.0006391291,0.0002125423,0.0002485871,0.0008301724,0.000222654],"domain_scores_gemma":[0.9975476,0.001318846,0.000319552,0.0003517856,0.0004170571,0.00004519366],"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.000309926,0.0002006084,0.001753487,0.0007987572,0.0001635349,0.001312288,0.000527085,0.6481425,0.04517357,0.2582636,0.002631144,0.04072349],"study_design_scores_gemma":[0.0001635939,0.000122731,0.000231625,0.00005576437,0.0000772102,0.0001580552,0.00004829319,0.9426744,0.02343942,0.02625123,0.006746286,0.00003145337],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01850214,0.0001104186,0.9743008,0.000168886,0.00007018079,0.000168181,0.0003325738,0.002686584,0.003660275],"genre_scores_gemma":[0.5467403,0.0004846204,0.4478792,0.0001664031,0.00002857651,0.0005695083,0.0008322799,0.0002254566,0.003073747],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.006325846,"threshold_uncertainty_score":0.01257807,"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."}}