{"id":"W2067623660","doi":"10.1007/s100090050045","title":"Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN","year":2000,"lang":"en","type":"article","venue":"International Journal on Software Tools for Technology Transfer","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":51,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Waterloo","funders":"","keywords":"Promela; Computer science; Common Object Request Broker Architecture; Model checking; Programming language; Protocol (science); Formal verification; Linear temporal logic; Formal specification; Theoretical computer science","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":[],"consensus_categories":[],"category_scores_codex":[0.0003824209,0.0001199279,0.0001302127,0.0002429602,0.0001358606,0.0001589201,0.0006560532,0.000139496,0.00001792502],"category_scores_gemma":[0.0001717661,0.00008949785,0.00006133223,0.0002091647,0.0001324214,0.0009568074,0.00005032383,0.000205538,8.134017e-7],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00006621621,"about_ca_system_score_gemma":0.00004614441,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000001784993,"about_ca_topic_score_gemma":6.428301e-7,"domain_scores_codex":[0.9989363,0.00005528078,0.0004032528,0.0002025559,0.0002625982,0.0001400064],"domain_scores_gemma":[0.99935,0.00004399201,0.0001089674,0.0001968411,0.0002704592,0.00002973618],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.0002296605,0.0001234594,0.004011258,0.00004590412,0.00008946114,0.00000309944,0.0003612586,0.0007521097,0.00690684,0.1190766,0.00002658077,0.8683738],"study_design_scores_gemma":[0.006948893,0.001979334,0.01392107,0.0008894952,0.00008218274,0.002672499,0.00006701586,0.1122046,0.7310315,0.09560372,0.03377856,0.0008211356],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.3197868,0.000006176845,0.6756921,0.0005418721,0.0001718145,0.003716978,0.000007843362,0.00005296338,0.00002343388],"genre_scores_gemma":[0.4180379,0.00002575136,0.578459,0.0002752698,0.000105627,0.002984639,0.000004049514,0.00002284114,0.00008497323],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.8675526,"threshold_uncertainty_score":0.3649617,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03510101619760418,"score_gpt":0.342277098449961,"score_spread":0.3071760822523568,"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."}}