{"id":"W4409253307","doi":"10.1007/978-3-031-87719-3_4","title":"Reusable Formal Model Libraries for Specifying and Analyzing Security Objectives in Event-B","year":2025,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Security and Verification in Computing","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":false,"ca_institutions":"Carleton University","funders":"","keywords":"Computer science; Event (particle physics); Formal methods; Software engineering; Programming language","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":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.001272245,0.0004130968,0.0005233206,0.001065583,0.0004800677,0.0009015261,0.002032232,0.0002894673,0.000002540904],"category_scores_gemma":[0.0002063496,0.0004323841,0.0001097685,0.0007479127,0.0004026017,0.001821376,0.001717587,0.0007104418,0.00000118448],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0002339371,"about_ca_system_score_gemma":0.0007391291,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001737442,"about_ca_topic_score_gemma":0.00007707583,"domain_scores_codex":[0.9968169,0.00003426119,0.0006142337,0.001436278,0.0004131089,0.0006852591],"domain_scores_gemma":[0.9976649,0.0009553603,0.0002619029,0.0008413019,0.0001739649,0.0001025428],"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.00002293204,0.00004137469,0.0003384815,0.0002741731,0.00001679651,0.00001228781,0.005765209,0.1431004,0.00004325165,0.5368052,0.00003542433,0.3135445],"study_design_scores_gemma":[0.0001960576,0.00004454857,0.00004291847,0.0003665855,0.00000340396,0.000006618025,0.000001004883,0.6397343,0.000418872,0.3587155,0.0001852931,0.000284908],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0003534875,0.001216558,0.9944654,0.0005104924,0.0007039141,0.0005126679,0.000007756626,0.0001133553,0.002116373],"genre_scores_gemma":[0.3470997,0.0001117064,0.6516612,0.0006253951,0.0002524249,0.00002251211,0.000005813979,0.00001995956,0.0002013008],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.4966339,"threshold_uncertainty_score":0.9998128,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02266178823953306,"score_gpt":0.2662824902534406,"score_spread":0.2436207020139075,"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."}}