{"id":"W4402757116","doi":"10.1016/j.jss.2024.112219","title":"A model-driven formal methods approach to software architectural security vulnerabilities specification and verification","year":2024,"lang":"en","type":"article","venue":"Journal of Systems and Software","topic":"Software Reliability and Analysis Research","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":false,"ca_institutions":"Carleton University; Université du Québec en Outaouais","funders":"","keywords":"Computer science; Formal methods; Software engineering; Software security assurance; Formal specification; Programming language; Model checking; Formal verification; Computer security; Information security; Security service","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.004839559,0.001069797,0.000843448,0.001600244,0.001033807,0.002703996,0.00320526,0.001594345,0.003670329],"category_scores_gemma":[0.009115661,0.001318966,0.002759855,0.0006511525,0.002631135,0.002282401,0.002290892,0.002987741,0.0007916775],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001700358,"about_ca_system_score_gemma":0.004436439,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.006135158,"about_ca_topic_score_gemma":0.007568401,"domain_scores_codex":[0.9966827,0.001413264,0.0002030736,0.0002464494,0.001279632,0.0001749444],"domain_scores_gemma":[0.9933037,0.004671014,0.0003177086,0.000904914,0.0006946042,0.0001080627],"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.00009382511,0.000281025,0.0008001238,0.0003688444,0.0001450645,0.0003082692,0.0005837273,0.3995665,0.01061286,0.4932529,0.002403624,0.09158339],"study_design_scores_gemma":[0.00006361167,0.00005336158,0.0001010718,0.00009575378,0.00006119231,0.00009625285,0.00005800471,0.799346,0.004900065,0.186395,0.008797066,0.00003263026],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.000931845,0.00003605744,0.9979051,0.0001152096,0.00001604793,0.0000585442,0.00002404322,0.0002529851,0.0006601624],"genre_scores_gemma":[0.07281263,0.000174337,0.9241998,0.0001282205,0.00003049966,0.0003852022,0.0001357303,0.0002382957,0.001895238],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.006135158,"threshold_uncertainty_score":0.02559429,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04063376757938385,"score_gpt":0.3236234408933789,"score_spread":0.282989673313995,"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."}}