[Sdn] SDN Application Verification

Nitin Shukla <nitin.csed@gmail.com> Thu, 19 May 2016 12:11 UTC

Return-Path: <nitin.csed@gmail.com>
X-Original-To: sdn@ietfa.amsl.com
Delivered-To: sdn@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id 91E8312B03D for <sdn@ietfa.amsl.com>; Thu, 19 May 2016 05:11:07 -0700 (PDT)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -2.699
X-Spam-Level:
X-Spam-Status: No, score=-2.699 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, FREEMAIL_FROM=0.001, HTML_MESSAGE=0.001, RCVD_IN_DNSWL_LOW=-0.7, SPF_PASS=-0.001] autolearn=ham autolearn_force=no
Authentication-Results: ietfa.amsl.com (amavisd-new); dkim=pass (2048-bit key) header.d=gmail.com
Received: from mail.ietf.org ([4.31.198.44]) by localhost (ietfa.amsl.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id C17CFoyPY6s1 for <sdn@ietfa.amsl.com>; Thu, 19 May 2016 05:11:06 -0700 (PDT)
Received: from mail-vk0-x244.google.com (mail-vk0-x244.google.com [IPv6:2607:f8b0:400c:c05::244]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 3B0B512B015 for <sdn@irtf.org>; Thu, 19 May 2016 05:11:06 -0700 (PDT)
Received: by mail-vk0-x244.google.com with SMTP id y2so3297422vka.0 for <sdn@irtf.org>; Thu, 19 May 2016 05:11:06 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:date:message-id:subject:from:to; bh=8Dz2Tu5uEigAQiexepNWgfucUAfKRwvowHONgMjZ6rM=; b=H9pIAjBlt64LgyIABx9DZe0L002ZOdgZMl0PgTN2Insgwzb2HhoKawWNl6PBmS4wUp cL9qjo3SNiiqdGyLdHyJGkQxae7fxSmvetBV+tWlr3piD8BsqR/ssmHVQrkG9UtDLuo/ 6B4lTzmXdNM69voE/yFEcNFuO6SVgVwU6VqcTYwrIqaFvrjdnpUPw/KzEBo3vOna9zul GfbNnSWuzKLsM37GdA+4Fm34CiLEXlZ9H9FcZVVsdZOiU7qWpWnTX6LzBEAx5wZDfYPF Hjlnb7BGeEGsbmEtbaFVtLiESYsPZmQJD6U3UF7OrdIvhuZFPVR920ef6q+WB4bKTY4T 9J7A==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:date:message-id:subject:from:to; bh=8Dz2Tu5uEigAQiexepNWgfucUAfKRwvowHONgMjZ6rM=; b=KQpb+Cmb6cql/iOwnY/2uLbKjMDuqHGFQJUAFiGZgrv5FSa1GMJSaWOciWSfZ/AZ26 3+BSQPOgVRqr6Y5066hMS0Dl9e2YjvqShxL6XavwgsTwjTT+DfzISEiIn8KMukHJZDgW fwmTbFBQvEv72oJXWvw9TzIo7Ab1J+1uZ6mpLYvSvf5mgFNM4hzMjBAoRbOafIKabzoe XXN16teLhidWVNddUzcz1y9LyyVzclJh/91WwjPEkVnBw2rx4NAw/xhfRA7w+Iv5hB2A rlQsiVSGvrWrLBR6rK7ixRPVoH94pL5ri/5O/4Qq3DIRSU5DZXFoDBW4ye6dt2N4/4lU K5Cw==
X-Gm-Message-State: AOPr4FUUHVntxbX4HCpl8azYh9e1ngq4Mvs7hhr05sAHr4F2+HZvayjhW8BRB8Ii1+u153QraCb3ROToL/ajAg==
MIME-Version: 1.0
X-Received: by 10.176.64.70 with SMTP id h64mr437236uad.10.1463659865303; Thu, 19 May 2016 05:11:05 -0700 (PDT)
Received: by 10.159.34.131 with HTTP; Thu, 19 May 2016 05:11:05 -0700 (PDT)
Date: Thu, 19 May 2016 17:41:05 +0530
Message-ID: <CAG_4AMKaHupvePOu4mRLMTgF0SXitm+OQtrs-yAk_LWnueZD-g@mail.gmail.com>
From: Nitin Shukla <nitin.csed@gmail.com>
To: sdn@irtf.org
Content-Type: multipart/alternative; boundary="94eb2c1228bc57f4d5053330de10"
Archived-At: <http://mailarchive.ietf.org/arch/msg/sdn/A2sCwIRRl3ir5BC91_W-ppjRgRE>
Subject: [Sdn] SDN Application Verification
X-BeenThere: sdn@irtf.org
X-Mailman-Version: 2.1.17
Precedence: list
List-Id: List to Discuss SDN Research Group in the IRTF <sdn.irtf.org>
List-Unsubscribe: <https://www.irtf.org/mailman/options/sdn>, <mailto:sdn-request@irtf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/sdn/>
List-Post: <mailto:sdn@irtf.org>
List-Help: <mailto:sdn-request@irtf.org?subject=help>
List-Subscribe: <https://www.irtf.org/mailman/listinfo/sdn>, <mailto:sdn-request@irtf.org?subject=subscribe>
X-List-Received-Date: Thu, 19 May 2016 12:15:33 -0000

Dear All,

Greetings.

I am Nitin Shukla, a research scholar at MNNIT Allahabad, Allahabad India.

I am currently working on a SDN project. I have coded an application using
Floodlight and mininet.

Now i am on to its formal verification so that i can prove that the flows
written on switches  are formally correct. I also want to formally verify
the correctness of my application.
So please suggest me some Formal modeling and verification tool which can
help me.


Thanks and Regards,

Nitin Shukla.
Research Scholar
(Department of Computer Science & Engineering)
Motilal Nehru National Institute of Technology,
Allahabad-211004, India.