{"id":"W1941952906","doi":"10.1109/ccece.2001.933562","title":"Model checking of the Fairisle ATM switch fabric using FormalCheck","year":2002,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":3,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"Computer science; Asynchronous Transfer Mode; Liveness; Asynchronous communication; Set (abstract data type); Verilog; Very-large-scale integration; Model checking; Code (set theory); Embedded system; Computer network; Programming language","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.001998855,0.0006435626,0.0004293648,0.0006360866,0.0006932565,0.001378664,0.001111354,0.0005186615,0.002688959],"category_scores_gemma":[0.006344829,0.0004416792,0.00127901,0.0002324644,0.002456537,0.001804121,0.0009326719,0.0008457293,0.0002053802],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001832571,"about_ca_system_score_gemma":0.002226094,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.006693466,"about_ca_topic_score_gemma":0.006116206,"domain_scores_codex":[0.9987122,0.0003889074,0.0000855984,0.0001811762,0.0004662035,0.0001659594],"domain_scores_gemma":[0.9963031,0.002368285,0.0003390689,0.0006365727,0.0002847176,0.00006823989],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0004752028,0.000132232,0.003527935,0.000284748,0.00007603967,0.000389872,0.0004837731,0.7982505,0.03849212,0.1295966,0.0009779178,0.02731306],"study_design_scores_gemma":[0.000153892,0.0002077921,0.0004607819,0.00004670859,0.0000677444,0.0001048884,0.00005714664,0.868193,0.0710481,0.05537258,0.004244788,0.00004246543],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.2016989,0.00012466,0.791564,0.0001899218,0.00005647037,0.00008208675,0.0002752781,0.00356779,0.002440914],"genre_scores_gemma":[0.8923464,0.0001046599,0.1049499,0.0000685378,0.00001886995,0.0001065134,0.0002526322,0.0001971918,0.001955253],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.006693466,"threshold_uncertainty_score":0.013309,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1477723592124317,"score_gpt":0.2922092801877091,"score_spread":0.1444369209752774,"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."}}