近十年以來(lái)，計(jì)算機(jī)科學(xué)研究的進(jìn)步大大推動(dòng)了需求和設(shè)計(jì)驗(yàn)證工具和技術(shù)的發(fā)展，其中最成功的技術(shù)當(dāng)屬模型校驗(yàn)。模型驗(yàn)證與規(guī)范化建模語(yǔ)言的緊密結(jié)合，極大地推動(dòng)了驗(yàn)證自動(dòng)化的發(fā)展。本文介紹了模型校驗(yàn)的原理及工作方式。 模型校驗(yàn)是最成功的需求驗(yàn)證工具。模型校驗(yàn)的基本原理如圖1所示。模型校驗(yàn)工具的輸入是系統(tǒng)需求或設(shè)計(jì)（稱為模型）以及最終系統(tǒng)期望實(shí)現(xiàn)的特性（稱為“規(guī)范”）。如果給定的模型滿足給定的規(guī)范，那么工具將輸出yes，否則將生成反例。反例詳細(xì)描述了模型無(wú)法滿足規(guī)范的原因，通過(guò)研究反例，可以精確地定位模型的缺陷，如此反復(fù)。該方法的原理是通過(guò)確保模型滿足足夠多的系統(tǒng)特性以增強(qiáng)我們對(duì)模型正確性的信心。系統(tǒng)需求之所以稱為模型，因?yàn)檫@些模型表征的是需求或設(shè)計(jì)。 那么，哪種規(guī)范化語(yǔ)言可以用來(lái)定義模型呢？答案當(dāng)然不是唯一的，因?yàn)椴煌瑧?yīng)用領(lǐng)域的需求（或設(shè)計(jì)）差異很大。例如，銀行系統(tǒng)和空間系統(tǒng)在系統(tǒng)規(guī)模、結(jié)構(gòu)、復(fù)雜度、系統(tǒng)數(shù)據(jù)的屬性及執(zhí)行操作上的需求差異就很明顯。相反，大多數(shù)實(shí)時(shí)嵌入式或安全臨界系統(tǒng)都面向控制，而不是數(shù)據(jù)，這意味著這些系統(tǒng)的動(dòng)態(tài)特性遠(yuǎn)比業(yè)務(wù)邏輯（由系統(tǒng)維護(hù)的內(nèi)部數(shù)據(jù)的結(jié)構(gòu)及操作）重要。這些基于控制的系統(tǒng)可以應(yīng)用于諸多領(lǐng)域：航天系統(tǒng)、航空電子、汽車系統(tǒng)、生物醫(yī)學(xué)儀器、工業(yè)自動(dòng)化及過(guò)程控制、鐵路、核電站等。甚至數(shù)字硬件系統(tǒng)的通信和安全協(xié)議均可視為面向控制的系統(tǒng)。圖1：模型校驗(yàn)方法。 對(duì)于面向控制的系統(tǒng)，可以采用有限狀態(tài)機(jī)（FSM）定義需求和設(shè)計(jì)，這是一種得到廣泛認(rèn)可的抽象表示方法。當(dāng)然，光靠FSM并不能對(duì)復(fù)雜的實(shí)際工業(yè)系統(tǒng)進(jìn)行建模。我們還需要：1. 能將需求模塊化并區(qū)分需求等級(jí)；2. 能合并各組成部分的需求（或設(shè)計(jì)）；3. 能通過(guò)更新預(yù)先規(guī)定的變量和設(shè)備，防止可能出現(xiàn)的異常。 校驗(yàn)設(shè)計(jì)需求時(shí)，通?？梢酝ㄟ^(guò)回答一些問(wèn)題得到結(jié)果。下面給出了校驗(yàn)需求時(shí)最常問(wèn)的一些問(wèn)題： ＊ 設(shè)計(jì)需求是否準(zhǔn)確地反映了用戶需求？需求中的每一事項(xiàng)是否與用戶的期望一致？需求是否包含用戶所要求的全部?jī)?nèi)容？ ＊ 設(shè)計(jì)需求是否表述清晰并無(wú)異義？是否能被用戶很好地理解？ ＊ 設(shè)計(jì)需求是否具有靈活性和可實(shí)現(xiàn)性？例如設(shè)計(jì)需求是否模塊化并具有良好的架構(gòu)，從而有助于設(shè)計(jì)和開(kāi)發(fā)？ ＊ 設(shè)計(jì)需求是否能輕松地定義驗(yàn)收測(cè)試示例以驗(yàn)證設(shè)計(jì)實(shí)現(xiàn)與需求的一致性。 ＊ 設(shè)計(jì)需求是否只是概要地描述而與具體的設(shè)計(jì)、實(shí)現(xiàn)及技術(shù)平臺(tái)等無(wú)關(guān)，從而使得設(shè)計(jì)人員和開(kāi)發(fā)人員具有充分的自由度實(shí)現(xiàn)這些需求？ 回答這些問(wèn)題當(dāng)然絕非輕而易舉而且也沒(méi)有任何捷徑可循，但如果需求成功地超越了這些條條框框，那么無(wú)疑為優(yōu)良系統(tǒng)的設(shè)計(jì)打下了堅(jiān)實(shí)基礎(chǔ)。盡管可以利用類似UML這樣的建模工具，但仍然需要確保設(shè)計(jì)需求的質(zhì)量。這個(gè)過(guò)程需要投入大量精力和時(shí)間，包括各種形式的審查，有時(shí)甚至還需要進(jìn)行部分原型設(shè)計(jì)。此外，需求設(shè)計(jì)中采用多種表示方法（如UML中的表示方法）通常又將引發(fā)其他的問(wèn)題,例如: ＊ 設(shè)計(jì)需求需要使用哪種表示方法？ ＊ 如何確保不同表示方法的描述的一致性？ 設(shè)計(jì)需求缺陷的成本通常很高，至少需要重設(shè)計(jì)并進(jìn)行維護(hù)。錯(cuò)誤的需求導(dǎo)致錯(cuò)誤的系統(tǒng)行為并顯著增加成本，如喪失產(chǎn)品的時(shí)效性和本質(zhì)特征，而對(duì)于工作在實(shí)時(shí)環(huán)境下的嵌入式安全臨界系統(tǒng)更是如此。為確保系統(tǒng)設(shè)計(jì)的質(zhì)量，也需要考慮類似的問(wèn)題。 改進(jìn)需求和設(shè)計(jì)的一條途徑是利用自動(dòng)化工具對(duì)需求和設(shè)計(jì)各環(huán)節(jié)的質(zhì)量進(jìn)行校驗(yàn)。那么，哪種工具最適用呢？一般而言，校驗(yàn)用英文描述的需求或設(shè)計(jì)極為困難。因此，必須采用一種清晰嚴(yán)格且無(wú)二義的規(guī)范化語(yǔ)言對(duì)需求進(jìn)行描述。如果這種描述需求和設(shè)計(jì)的語(yǔ)言具有明確的語(yǔ)義，那么完全可以開(kāi)發(fā)出自動(dòng)化工具以分析這種語(yǔ)言描述的設(shè)計(jì)需求。這種采用嚴(yán)格語(yǔ)言描述需求或設(shè)計(jì)的基本思想已成為系統(tǒng)驗(yàn)證的基石。 簡(jiǎn)單的系統(tǒng)模型實(shí)例 首先，讓我們考察一下如何利用模型校驗(yàn)工具驗(yàn)證簡(jiǎn)單的嵌入式系統(tǒng)特性。為此，我們采用Carnegie-Mellon大學(xué)開(kāi)發(fā)的符號(hào)模型驗(yàn)證器（symbolic model verifier,SMV）作為模型校驗(yàn)工具。當(dāng)然，我們也可以采用其他的模型校驗(yàn)工具描述該模型。文章結(jié)束部分列出了可選的模型校驗(yàn)工具及獲取方式。 如圖2所示，一個(gè)簡(jiǎn)單的泵控系統(tǒng)通過(guò)泵P將源水槽A中的水傳送至接收水槽B。每個(gè)水槽都具有兩級(jí)刻度線：一個(gè)用來(lái)檢測(cè)水位是否為空（Empty），而另一個(gè)用來(lái)檢測(cè)水位是否已滿（Full）。如果水槽的水位既不為空也不為滿，那么水槽刻度線設(shè)定為ok；換言之，即水位高于空刻度線但低于滿刻度線。 最初，兩個(gè)水槽均為空。一旦水槽A的水位值為ok（從空開(kāi)始），啟動(dòng)泵并假定水槽B尚未為滿。只要水槽A不為空且水槽B不為滿，泵將持續(xù)工作。一旦水槽A為空或水槽B為滿，泵將停止工作。一旦泵啟動(dòng)（或停止），系統(tǒng)將不會(huì)嘗試停止（或啟動(dòng)）泵。雖然這個(gè)示例非常簡(jiǎn)單，但可以很容易地?cái)U(kuò)展為控制多個(gè)源水槽和接收水槽的復(fù)雜泵管線網(wǎng)絡(luò)控制器，如應(yīng)用在水處理系統(tǒng)或化工廠中的控制器。 表1：SMV模型描述和需求清單。 MODULE main VAR level_a : ｛Empty, ok, Full｝; —— lower tank level_b : ｛Empty, ok, Full｝; —— upper tank pump : ｛on, off｝; ASSIGN next（level_a） := case level_a = Empty : ｛Empty, ok｝; level_a = ok & pump = off : ｛ok, Full｝; level_a = ok & pump = on : ｛ok, Empty, Full｝; level_a = Full & pump = off : Full; level_a = Full & pump = on : ｛ok, Full｝; 1 : ｛ok, Empty, Full｝; esac; next（level_b） := case level_b = Empty & pump = off : Empty; level_b = Empty & pump = on : ｛Empty, ok｝; level_b = ok & pump = off : ｛ok, Empty｝; level_b = ok & pump = on : ｛ok, Empty, Full｝; level_b = Full & pump = off : ｛ok, Full｝; level_b = Full & pump = on : ｛ok, Full｝; 1 : ｛ok, Empty, Full｝; esac; next（pump） := case pump = off & （level_a = ok | level_a = Full） & （level_b = Empty | level_b = ok） : on; pump = on & （level_a = Empty | level_b = Full） : off; 1 : pump; —— keep pump status as it is esac; INIT （pump = off） SPEC —— pump if always off if ground tank is Empty or up tank is Full —— AG AF （pump = off -> （level_a = Empty | level_b = Full）） —— it is always possible to reach a state when the up tank is ok or Full AG （EF （level_b = ok | level_b = Full）） 系統(tǒng)狀態(tài)就可用上述3個(gè)變量的不同取值來(lái)表示。例如（level_a=Empty, level_b=ok, pump=off）和l （level_a=Empty, level_b=Full, pump=on）就可以表示系統(tǒng)狀態(tài)。在靠近結(jié)尾的INIT部分，定義了這些變量的初始值（這里，最初假定pump的初始值為off，而其他兩個(gè)變量則可取任意值）。 ASSIGN部分定義了系統(tǒng)如何從一個(gè)狀態(tài)遷移到另一個(gè)狀態(tài)。每個(gè)next語(yǔ)句都規(guī)定了特定變量的取值變化。所有這些賦值語(yǔ)句都假定可以并行執(zhí)行；next語(yǔ)句定義為在該部分執(zhí)行所有賦值語(yǔ)句后的最終結(jié)果。下層水槽的狀態(tài)可以從Empty狀態(tài)遷移到Empty或ok狀態(tài)；從ok狀態(tài)遷移到Empty或Full狀態(tài)，或保持為ok狀態(tài)（如果pump的狀態(tài)為on）；從ok狀態(tài)遷移到ok或Full狀態(tài)（如果pump的狀態(tài)為off）；如果pump狀態(tài)為off，那么下層水槽在Full狀態(tài)無(wú)法發(fā)生狀態(tài)遷移；如果泵狀態(tài)為on，則可遷移到ok或Full狀態(tài)。上層水槽也可規(guī)定類似的操作。 在系統(tǒng)內(nèi)部，大多數(shù)模型校驗(yàn)工具通常會(huì)將輸入模型擴(kuò)展為具有Kripke結(jié)構(gòu)的動(dòng)態(tài)系統(tǒng)。擴(kuò)展過(guò)程包括在EFSM中除去分層結(jié)構(gòu)、并行成分以及狀態(tài)遷移時(shí)的告警和操作。Kripke結(jié)構(gòu)中的每個(gè)狀態(tài)實(shí)際上都可用每個(gè)狀態(tài)均賦值的元組（tuple）來(lái)表示。Kripke結(jié)構(gòu)中的狀態(tài)遷移表征了一個(gè)或多個(gè)狀態(tài)變量取值的變化；而且還可以比較通過(guò)擴(kuò)展給定模型而得到的Kripke結(jié)構(gòu)，對(duì)指定的系統(tǒng)屬性進(jìn)行校驗(yàn)。然而，為了更好地理解每條屬性語(yǔ)句的含義，Kripke結(jié)構(gòu)還必須進(jìn)一步擴(kuò)展為無(wú)限樹(shù)形結(jié)構(gòu)，其中樹(shù)形結(jié)構(gòu)的每個(gè)分支都表征了系統(tǒng)可能的執(zhí)行操作或行為。 路徑和屬性規(guī)范 最開(kāi)始，系統(tǒng)可以處于9個(gè)狀態(tài)中的任意一個(gè)，其中對(duì)于A和B的水位沒(méi)有任何限制，而pump的初始狀態(tài)假定為off。這樣，我們就可以利用有序元組表征狀態(tài)，其中A和B分別表示水槽A和B的當(dāng)前水位，而P則表示pump的當(dāng)前狀態(tài)。例如，可以假定系統(tǒng)的初始狀態(tài)為。對(duì)于系統(tǒng)模型，初始狀態(tài)之后的下一個(gè)狀態(tài)可以為和中的任意一個(gè)。從狀態(tài)開(kāi)始，下一個(gè)狀態(tài)可以為、、、、或中的任意一個(gè)。根據(jù)每個(gè)狀態(tài)，可以計(jì)算出下一個(gè)可能的狀態(tài)。 這些狀態(tài)可以無(wú)限執(zhí)行（或運(yùn)算）樹(shù)狀結(jié)構(gòu)的形式進(jìn)行排列。如圖3所示，樹(shù)根為我們所選的初始狀態(tài)，任意狀態(tài)的分支均表示下一個(gè)可能的狀態(tài)，而每個(gè)系統(tǒng)執(zhí)行都是執(zhí)行樹(shù)狀結(jié)構(gòu)的一條路徑?？傮w上，系統(tǒng)可以具有無(wú)限多個(gè)這樣的執(zhí)行路徑。模型校驗(yàn)的目標(biāo)就是檢驗(yàn)執(zhí)行樹(shù)狀結(jié)構(gòu)是否滿足用戶指定的屬性要求。 現(xiàn)在的問(wèn)題在于，我們究竟該如何描述執(zhí)行樹(shù)狀結(jié)構(gòu)路徑（及路徑上的狀態(tài)）的屬性。從技術(shù)的角度看，運(yùn)算樹(shù)邏輯（Computation tree logic, CTL）是時(shí)序邏輯（time temporal logic, TTL）的一個(gè)分支，其簡(jiǎn)單性和直觀性非常適合于本例。CTL是常用的布爾命題邏輯（Boolean propositional logic, BPL）的擴(kuò)展，除了支持包括“和（and）”、“或（or）”、“否（not）”、“蘊(yùn)涵（implies）”在內(nèi)的BPL邏輯連接操作外，還支持輔助的時(shí)序連接操作。表2所示為 CTL 中的某些連接操作。 表1和圖4說(shuō)明了CTL中一些基本時(shí)序連接操作的直觀意義。一般地，E（就某個(gè)路徑而言）和A（就所有的路徑而言）表示從某個(gè)狀態(tài)開(kāi)始的路徑數(shù)目。F（就某個(gè)狀態(tài)而言）和G（就所有狀態(tài)而言）表示某個(gè)路徑中的狀態(tài)數(shù)目。 對(duì)于指定的屬性以及對(duì)應(yīng)于系統(tǒng)模型的運(yùn)算樹(shù)T（可以是無(wú)限運(yùn)算樹(shù)），模型校驗(yàn)算法可以通過(guò)校驗(yàn)T判斷T是否滿足該屬性。例如，考慮指定的屬性AF g，其中g(shù)表示與任何CTL連接無(wú)關(guān)的命題公式。圖4b給出了運(yùn)算樹(shù)T的一個(gè)示例。如果屬性AF g在根狀態(tài)s0的值設(shè)定為true（即如果T中的每條路徑中有狀態(tài)開(kāi)始于s0以使公式g為true），那么對(duì)于該運(yùn)算樹(shù)TAF g的值為true。如果g在s0為true，那么就實(shí)現(xiàn)了預(yù)定目標(biāo)，因?yàn)閟0將會(huì)出現(xiàn)在從s0開(kāi)始的每條路徑中。但如果g在s0狀態(tài)下不為true，由于從s0開(kāi)始的路徑要么是s0的左分支，要么是s0的右分支，因此如果在運(yùn)算樹(shù)T中s0的兩個(gè)分支都為true（通過(guò)遞歸校驗(yàn)），那么該屬性在s0處也為true。 圖4b顯示，g在左分支根部為true（球體填充為黃色）。因此從s0到左分支單元的所有路徑以及整個(gè)左分支樹(shù)都滿足該屬性?，F(xiàn)在假定g在s0的右分支根部不為true；因此對(duì)于所有的子單元都將遞歸檢驗(yàn)該屬性。圖4b顯示，對(duì)于s0右分支的所有子單元，g都為true（球體填充為黃色），因此對(duì)于s0的右分支樹(shù)該屬性為true。這樣，對(duì)于s0的所有子分支樹(shù)該屬性為true，從而s0也為true。 圖4歸納了類似的其他屬性（例如EG g和AG g）校驗(yàn)原理。當(dāng)然，實(shí)際應(yīng)用中的模型校驗(yàn)算法遠(yuǎn)比這復(fù)雜；這些算法利用一些巧妙的簡(jiǎn)化手段對(duì)狀態(tài)空間進(jìn)行精簡(jiǎn)，從而避免了對(duì)那些確保為true的屬性進(jìn)行校驗(yàn)。一些設(shè)計(jì)良好的模型校驗(yàn)器可用來(lái)校驗(yàn)狀態(tài)數(shù)高達(dá)1,040個(gè)的狀態(tài)空間的屬性。在SMV中，待驗(yàn)證的屬性可由SPEC部分的用戶指定。邏輯連接“否”、“或”、“和”和“if-then”可以分別用!、|、&和 ->表示。CTL時(shí)序連接則表示為AF、AG、EF、EG等。屬性AF（pump=on）表示對(duì)于每條開(kāi)始于初始狀態(tài)的路徑，路徑中有一個(gè)pump=on的狀態(tài)。在初始狀態(tài)，該屬性顯然為false，因?yàn)閺某跏紶顟B(tài)開(kāi)始有一條路徑pump的值始終為off（例如，當(dāng)水槽A永遠(yuǎn)保持為空時(shí)）。如果希望在SPEC部分中描述該屬性，那么SMV將為該屬性生成如下反例。循環(huán)表征了開(kāi)始于初始狀態(tài)的無(wú)限狀態(tài)序列（換言之，即路徑），這樣水槽B在該路徑下的每個(gè)狀態(tài)均為Full，因此pump=off。 與嚴(yán)格的規(guī)范化語(yǔ)言相結(jié)合，可以下列執(zhí)行序列表示： state 1.1: level_a = Full level_b = Full pump = off state 1.2: 屬性AF（pump=off）具有兩重含義，表征的是對(duì)于每條開(kāi)始于初始狀態(tài)的路徑，路徑中有一個(gè)狀態(tài)中pump=off。該屬性當(dāng)然在初始狀態(tài)為true，因?yàn)槌跏紶顟B(tài)本身（所有路徑均包含初始狀態(tài)）pump=off就成立。 時(shí)序連接和邏輯連接相結(jié)合，可以得到一些有趣的復(fù)雜屬性。屬性AG（（pump=off） -> AF （pump=on））表示如果pump=off，那么最終pump=on這種情形總會(huì)發(fā)生。初始狀態(tài)，該屬性顯然為false。屬性AG AF （pump=off -> （level_a=Empty | level_b=Full））表示如果底層水槽為Empty或上層水槽為Full，那么pump將總是為off。屬性AG （EF （level_b= ok|level_b=Full））表示總是會(huì)出現(xiàn)上層水槽為ok或Full的情形。 實(shí)際應(yīng)用中的模型校驗(yàn) 模型校驗(yàn)已被證明是對(duì)各類系統(tǒng)（尤其是硬件系統(tǒng)、實(shí)時(shí)嵌入式系統(tǒng)和安全臨界系統(tǒng)）進(jìn)行需求和設(shè)計(jì)驗(yàn)證的有效工具。例如，SPIN模型校驗(yàn)器曾用于驗(yàn)證NASA的深空1發(fā)射方案中的多線程規(guī)劃執(zhí)行模型并成功地發(fā)現(xiàn)了5個(gè)先前未知的并發(fā)缺陷。然而，實(shí)際使用模型校驗(yàn)時(shí)還需要注意下面一些主要問(wèn)題： 1. 每種模型校驗(yàn)工具都采用特有的建模語(yǔ)言，這些建模語(yǔ)言一般都無(wú)法將不規(guī)范的需求描述自動(dòng)轉(zhuǎn)化為規(guī)范化語(yǔ)言。這樣的轉(zhuǎn)化顯然需要手工完成，因此很難檢驗(yàn)?zāi)Ｐ褪欠裾_地表示了建模系統(tǒng)。實(shí)際上，指定的建模表示法往往很難甚至根本不可能對(duì)部分系統(tǒng)需求進(jìn)行建模。2. 專用工具屬性規(guī)范表示法也存在類似的問(wèn)題，屬性表示法通?？梢允荂TL、CTL＊或命題線性時(shí)序邏輯（PLTL）的變形。某些需要驗(yàn)證的屬性很難甚至根本不可能用該表示法進(jìn)行描述。3. 模型系統(tǒng)中的狀態(tài)數(shù)量也可能極為龐大。盡管模型校驗(yàn)算法可以利用一些技巧減小狀態(tài)空間的復(fù)雜度，但模型校驗(yàn)器仍然需要很長(zhǎng)的時(shí)間才能驗(yàn)證一個(gè)指定的屬性或者決定“放棄”驗(yàn)證該屬性。這時(shí)，用戶將不得不投入更大的精力，獨(dú)立驗(yàn)證模型的各部分或者通過(guò)減小變量的取值范圍以達(dá)到簡(jiǎn)化狀態(tài)空間的目的。 盡管如此，模型校驗(yàn)仍被證明是無(wú)與倫比的系統(tǒng)需求或設(shè)計(jì)驗(yàn)證工具。該工具能在需求或設(shè)計(jì)的早期階段發(fā)現(xiàn)瑕疵，因此能極大地節(jié)省后續(xù)的開(kāi)發(fā)時(shí)間。 鳴謝 衷心感謝Tata研發(fā)和設(shè)計(jì)中心（TRDDC）的常務(wù)董事Mathai Joseph教授對(duì)我的大力支持。我也非常感激Manasee Palshikar博士對(duì)我的鼓勵(lì)和支持。 參考文獻(xiàn) 1. Clarke, Edmund M., Orna Grumberg, and Doron A. Peled. Model Checking, Cambridge, MA: MIT Press, 1999.2. Berard, Beatrice, Michel Bidoit, Alain Finkel, Francois Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen, and Pierre Mckenzie. Systems and Software Verification: Model-Checking Techniques and Tools, Berlin-Heidelberg: Springer Verlag, 2001. 3. Havelund, Klaus, Mike Lowry, and John Penix. "Formal Analysis of a Space-Craft Controller using SPIN," IEEE Transactions on Software Engineering, vol. 27, no. 8, Aug. 2001, pp. 749-765. 4. Clarke, Edmund M., Orna Grumberg, and Doron A. Peled. Model Checking, Cambridge, MA: MIT Press, 1999. 5. Berard, Beatrice, Michel Bidoit, Alain Finkel, Francois Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen, and Pierre Mckenzie. Systems and Software Verification: Model-Checking Techniques and Tools, Berlin-Heidelberg: Springer Verlag, 2001. 6. Havelund, Klaus, Mike Lowry, and John Penix. "Formal Analysis of a Space-Craft Controller using SPIN," IEEE Transactions on Software Engineering, vol. 27, no. 8, Aug. 2001, pp. 749-765. 7. Harel, David, and Michal Politi. Modeling Reactive Systems with Statecharts—The Statemate Approach. New York, NY: McGraw-Hill, 1998. 作者：Girish Keshav Palshikar，Tata研發(fā)和設(shè)計(jì)中心科學(xué)家，Email: girishp@pune.tcs.co.in