{"id":"W4386515768","doi":"10.1007/978-3-031-40436-8_13","title":"Applying Formal Verification to an Open-Source Real-Time Operating System","year":2023,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Software Testing and Debugging Techniques","field":"Computer Science","cited_by":4,"is_retracted":false,"has_abstract":false,"ca_institutions":"Simon Fraser University","funders":"","keywords":"Promela; Computer science; Rotation formalisms in three dimensions; Programming language; Variety (cybernetics); Model checking; Semantics (computer science); Formal methods; Formal specification; Code (set theory); Formal verification; Specification language; Software engineering; Artificial intelligence","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","scholarly_communication","open_science"],"consensus_categories":[],"category_scores_codex":[0.00268121,0.0005016983,0.000549691,0.0008449458,0.0007140328,0.002344267,0.006990956,0.0002740594,0.000002772422],"category_scores_gemma":[0.0002688713,0.0004880244,0.00005942488,0.001054463,0.0001629178,0.001468082,0.004187761,0.0005274874,0.0001675607],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0004486913,"about_ca_system_score_gemma":0.0004292037,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0002687535,"about_ca_topic_score_gemma":0.00001891879,"domain_scores_codex":[0.9957344,0.00006533949,0.0006189506,0.00188829,0.0009063379,0.0007866915],"domain_scores_gemma":[0.9963238,0.0006150972,0.0002894312,0.002192139,0.0003016355,0.00027789],"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.000004067986,0.00001756927,0.0000480507,0.00006435587,0.00000561144,0.00004779495,0.001207826,0.03012827,0.0006828535,0.01301117,0.0001548085,0.9546276],"study_design_scores_gemma":[0.000134485,0.0003572054,0.00009054257,0.001393365,0.000005818377,0.0001069845,4.184511e-7,0.971405,0.0009081396,0.02429409,0.000471645,0.0008322704],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.000123801,0.00001343043,0.984719,0.0001682422,0.0007448636,0.001286272,0.000003778894,0.009953564,0.002987055],"genre_scores_gemma":[0.05834284,0.000003894262,0.9396712,0.0006818273,0.0003865294,0.0002065166,0.00001322785,0.00008932893,0.0006045942],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9537954,"threshold_uncertainty_score":0.9997572,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03405798701312469,"score_gpt":0.2820889373204126,"score_spread":0.2480309503072879,"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."}}