{"id":"W2055102535","doi":"10.4204/eptcs.13.6","title":"Verifying Real-Time Systems using Explicit-time Description Methods","year":2009,"lang":"en","type":"article","venue":"Electronic Proceedings in Theoretical Computer Science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":true,"ca_institutions":"St. Francis Xavier University","funders":"Natural Sciences and Engineering Research Council of Canada; Atlantic Canada Opportunities Agency","keywords":"Process (computing); Modularity (biology); Rotation formalisms in three dimensions; Synchronization (alternating current); Model checking; Rendezvous; Semaphore; Asynchronous communication","routes":{"ca_aff":true,"ca_fund":true,"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.005373893,0.001011808,0.0007284842,0.0009689475,0.0005060982,0.001833198,0.002197678,0.00100447,0.001686967],"category_scores_gemma":[0.01161528,0.0007720808,0.001584084,0.0007353409,0.001715291,0.003472593,0.001792329,0.001456638,0.0003640252],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001112958,"about_ca_system_score_gemma":0.002119535,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00199672,"about_ca_topic_score_gemma":0.00228912,"domain_scores_codex":[0.9935662,0.00291509,0.0006079838,0.0005702485,0.002060717,0.0002798722],"domain_scores_gemma":[0.9897465,0.006166962,0.0009159285,0.002269119,0.0008019786,0.00009962369],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0004491067,0.0002059282,0.002115487,0.0009277047,0.0002322326,0.0007413618,0.0008805409,0.4753841,0.02824291,0.3118301,0.001876367,0.1771142],"study_design_scores_gemma":[0.0002437299,0.0001051507,0.0002235263,0.0001223925,0.00009659256,0.0003071978,0.00005321021,0.8920337,0.03516083,0.05775357,0.01383588,0.00006428263],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.004291059,0.00008383895,0.9940822,0.00004011707,0.00001385978,0.00005080674,0.00003358194,0.0008928578,0.0005117517],"genre_scores_gemma":[0.2237857,0.0004381102,0.7725567,0.0001069589,0.00002775502,0.0003315852,0.0003401765,0.0003338789,0.002079112],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.005373893,"threshold_uncertainty_score":0.02842021,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02040135599401856,"score_gpt":0.319022635246982,"score_spread":0.2986212792529634,"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."}}