{"id":"W3108573523","doi":"10.1109/tvt.2020.3040817","title":"Formal Verification and Performance Analysis of a New Data Exchange Protocol for Connected Vehicles","year":2020,"lang":"en","type":"article","venue":"IEEE Transactions on Vehicular Technology","topic":"Distributed systems and fault tolerance","field":"Computer Science","cited_by":15,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Ottawa","funders":"","keywords":"MQTT; Computer science; Message queue; Correctness; Protocol (science); Promela; Workload; Computer network; Context (archaeology); Distributed computing; Protocol data unit; Real-time computing; Model checking; Database; Embedded system; Operating system; Programming language; Network packet","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.0001277031,0.0001204885,0.0002791314,0.0002794274,0.0001149586,0.00002977227,0.0007470041,0.000150982,0.000005386255],"category_scores_gemma":[0.00001038761,0.0001140179,0.00005939161,0.001642106,0.00006084652,0.0004113777,0.00001198623,0.0001291812,0.000002751598],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00001342184,"about_ca_system_score_gemma":0.00004989384,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001317441,"about_ca_topic_score_gemma":0.00001789223,"domain_scores_codex":[0.9989353,0.0000184753,0.0002872236,0.0004381412,0.0001302407,0.0001906613],"domain_scores_gemma":[0.9989243,0.00002738745,0.0001350002,0.0007496054,0.00009680472,0.00006689663],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0004430447,0.0004200214,0.0005541727,0.0007564243,0.001369656,0.000006294959,0.001188426,0.01231553,0.02248796,0.004865245,0.0008824599,0.9547108],"study_design_scores_gemma":[0.001161591,0.0004601183,0.0006323563,0.00003006485,0.0001333119,0.000004838411,0.00004501153,0.9566807,0.02992803,0.00003615215,0.01073619,0.0001516376],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02240572,0.00001824079,0.9632522,0.001586683,0.00003108854,0.01237782,0.0001163806,0.0002028102,0.000009086827],"genre_scores_gemma":[0.9741812,0.000007512574,0.01021641,0.00009420484,0.00001310872,0.01544471,0.00002046853,0.000007950614,0.00001438524],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.9545591,"threshold_uncertainty_score":0.4649516,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0598362794014457,"score_gpt":0.2963799131618651,"score_spread":0.2365436337604194,"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."}}