{"id":"W2526915519","doi":"10.1109/tsc.2015.2449850","title":"Using π-calculus for Formal Modeling and Verification of WS-CDL Choreographies","year":2015,"lang":"en","type":"article","venue":"IEEE Transactions on Services Computing","topic":"Service-Oriented Architecture and Web Services","field":"Computer Science","cited_by":9,"is_retracted":false,"has_abstract":true,"ca_institutions":"Institute of Health Economics","funders":"","keywords":"Correctness; Computer science; Choreography; Programming language; Workflow; Orchestration; Web service; Formal verification; Promela; Model checking; Software engineering; Formal methods; Modeling language; Process calculus; Formal specification; Database; Software","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.00475049,0.0006653729,0.0006876509,0.001090809,0.001573156,0.002637878,0.001758313,0.001025568,0.001850999],"category_scores_gemma":[0.009176691,0.0008321838,0.002181939,0.0008308055,0.003422445,0.00282761,0.002098477,0.002256038,0.0004572885],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002004271,"about_ca_system_score_gemma":0.006438947,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.01129933,"about_ca_topic_score_gemma":0.007394119,"domain_scores_codex":[0.9963484,0.001038689,0.0003538487,0.0004053551,0.001506833,0.0003468657],"domain_scores_gemma":[0.9962042,0.002164755,0.0003729393,0.0006619642,0.0004890416,0.0001071409],"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.00009307859,0.0001088364,0.001492114,0.0002793966,0.00007976847,0.0008729465,0.0008307541,0.1948945,0.01160738,0.7577326,0.001218988,0.03078953],"study_design_scores_gemma":[0.00009497229,0.0000647522,0.0002734653,0.0001313105,0.00009721364,0.0002128412,0.0001165867,0.693845,0.02317706,0.2566868,0.02522189,0.00007821131],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.003985855,0.00006687338,0.9931632,0.00009827744,0.0000438914,0.00007979429,0.00004472756,0.0007886075,0.001728759],"genre_scores_gemma":[0.2485211,0.0005875778,0.7458641,0.0001684759,0.00006711422,0.0005842582,0.0002315366,0.000344024,0.003631911],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01129933,"threshold_uncertainty_score":0.0251233,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04881808864591793,"score_gpt":0.2831887422336691,"score_spread":0.2343706535877512,"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."}}