{"id":"W6920314575","doi":"10.60692/awv1s-dn266","title":"Formal Verification and Performance Analysis of a New Data Exchange Protocol for Connected Vehicles","year":2020,"lang":"en","type":"article","venue":"Greater South Information System","topic":"Vehicular Ad Hoc Networks (VANETs)","field":"Engineering","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Ottawa","funders":"","keywords":"MQTT; Correctness; Message queue; Workload; Protocol (science); Protocol data unit; Promela; Model checking; Formal verification; Communications protocol","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.005016038,0.0006992542,0.0006018956,0.001192299,0.0008387531,0.002534219,0.001598181,0.001119311,0.002736281],"category_scores_gemma":[0.01568638,0.0005358988,0.001539828,0.0006000907,0.002490798,0.002520009,0.00218559,0.001806015,0.0003555347],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001987791,"about_ca_system_score_gemma":0.003516899,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004859335,"about_ca_topic_score_gemma":0.002663553,"domain_scores_codex":[0.9932786,0.001692664,0.0004671183,0.0008010857,0.003195984,0.0005646467],"domain_scores_gemma":[0.9912338,0.005213515,0.0007254409,0.001169719,0.001516467,0.0001410953],"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.0003789269,0.0003300687,0.003178614,0.0007043951,0.0001675863,0.001045943,0.0006886416,0.51094,0.02795373,0.4106005,0.00184153,0.04217012],"study_design_scores_gemma":[0.00008664661,0.0001622004,0.0003284028,0.00005418009,0.00006718224,0.0001543989,0.00004968853,0.9483293,0.0117061,0.03420252,0.004830956,0.00002830306],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.03254709,0.0001688982,0.961641,0.0003177671,0.00009286065,0.0002564033,0.0001523496,0.001367831,0.003455709],"genre_scores_gemma":[0.8010193,0.0003377708,0.1938563,0.0001416786,0.00008814287,0.0004959448,0.000400125,0.0002276614,0.00343312],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.005016038,"threshold_uncertainty_score":0.0265277,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.07969185783996179,"score_gpt":0.2413014151526076,"score_spread":0.1616095573126459,"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."}}