HARPO Programming Language Design
HARPO stands for HARdware Programming with Objects. HARPO/L is a programming language for hardware/software codesign. The language is based on the idea of a network of cooperating, multi- threaded objects. I have been designing the language and investigating methods of compiling it and similar languages to programmable hardware such as Coarse-Grained Reconfigurable Architectures. Currently we are looking at methods of proving concurrent programs free of certain classes of error and that they meet their specifications.
Poster
 |
|
Formal Verification of HARPO
This paper reports an implementation of a verifier for HARPO, a concurrent programming language. The verifier translates annotated programs into the intermediate verification language Boogie; the translated program is then checked by the Boogie verifier. The translation of HARPO programs is achieved by parsing the source code into valid abstract syntax tree; each node of the syntax tree is then used for generating its equivalent Boogie code. By using our verifier, HARPO programmers can be assured that their designs are free of defects.
Read Full Text
Errors in the software are hazardous. Testing software, before its deployment, may catch some errors present in the software. However, testing does not guarantee their absence. Several formal verification tools have been built and used for formal verification to ensure the correctness of software in different programming languages. The Boogie language is a common intermediate representation for static verification of programs written in several high-level programming languages. In this paper, notable software verifiers such as Dafny, VCC, HAVOC, Verve, and Chalice are described and analyzed for similarities and dissimilarities with the HARPO verifier.
Read Full Text
HARPO (HARdware Parallel Objects) is a concurrent programming language designed to run on coarse-grained reconfigurable computing architectures, Field Programmable Gate Arrays (FPGAs), and Graphicaal Processing Units (GPUs). The HARPO compiler translates programs into Boogie for verification and into VHDL for implementation on FPGA. Writing specifications and annotations in HARPO language for a hardware design shortens the development time and bridges the gap between high-level programming languages and hardware description languages. In this paper, the design of an integer “Counter” is verified using HARPO Verifier by translating the program into Boogie. Various counting scenarios containing explicit transfer of permissions have been verified using HARPO verifier. The correctness of design must be verified before translating and implementing the design on FPGA.
Read Full Text
Dafny Interactive Theorem Prover
Formal program verification has been used as a technique to ensure program correctness for several years. In this paper, the backend of formal verification system, named Boogie IVL, is discussed using interactive verifier named the Dafny. In this paper, the Dafny language and verifier are reviewed in detail. Some important features which are unavailable in high level programming languages like Java, C, and, Python but the Dafny language has direct support for those features namely sets, sequences, and, termination matric etc. The Dafny IDE and its integration available with Visual Studio is being used as verifier of a complete software system. It supports modularity, generic classes, abstraction, and, reverification. The Dafny compiler can produce both .NET executable code and verification conditions for Boogie Verification Debugger. We have also analysed the verification results of algorithms named, bubble sort, nth fibonacci number, and, schorr waite with benefits of using Dafny IDE. When the Dafny language was designed some essential techniques in formal verification namely, verification-splitting and timeout had not received attention by its developers. These features are highlighted in this paper, and we found that as compared to other verifiers e.g VCC, Eiffel, and, Spec# the Dafny verifier IDE has more interactive program verification system.
Read Full Text
In-Memory Processing with Micron Automata Processors
Since IoT is an information technology buzzword today, and In-Memory Computation is a highly parallel processing architecture of comprehensive search and analysis. There is no standard architecture for IoT, exploring the architectural aspects of authentication of things connected to others via the Internet and small networks. This process is compulsory before joining the internet either it is Web of Things, Machine to Machine, or Human to Machine frame of communication. For connected moveable devices or objects when they switch from one network to another, their connectivity to the network must be ensured, and on the other side when intrusion encountered from outside the IoT environment it must be handled by the security policy implemented on servicing computing machine. This search is as simple to implement with hash tables, but hashing becomes inefficient when entries become more significant and not scalable. Devices profiles and firewalls for authentication and intrusion detection/prevention must be maintained after they are authenticated. When thousands of devices need to get connected with IoT environment then managing their authentication and intrusion blocking policies must be performed quickly and giving an impression of dedicated service response from the server machine. These high-performance servers are implemented with MIMD machines. Accelerating service of requests from IoT’s low-end devices using In-Memory Computation is will be a new approach for comprehensive search and analysis. The technique of Automata Processing used for search of device identity speed up the processes of authentication if implemented on Micron Automata Processor, an In-Memory Computing Architecture. In this report with amalgamation of IoT and Non-Von Neuman Architecture with a new approach of authentication with their background and viability study.
Read Full Text
Telemedicine Web Applications
Telemedicine services increase the quality and accessibility of healthcare services. In this project named “Web Based ECG Monitoring System” we develop ECG monitoring which has potential to address diverse diseases in human body and by increasing the quality of treatment. Monitor Patients in remote area where clinical services such as ECG are not available. Off the shelf Arduino based shields can be deployed to monitor patients ECG in a cheaper way at home, military camps, remote non clinical areas and small size hospitals, home and middle class communities comparatively to the conventional clinical system. Use of already existing Internet is a major breakthrough in our idea. More than 100 diseases and their abnormalities in human body can be detected by remote physician using this implementation. In data acquisition module, programming Arduino based shields to acquire data from electrical activities of heart or muscles sending data using USB interfacing which will be stored in PC and upload on website named “www. hostpkdesgins. com” where doctor can visually see this information and complete prescriptions can be given by doctor. Here doctor can also serve more patients than conventional ECG systems. Use of same technology implementation we can develop system based on electromyogram, electroencephalogram and many more but the problem is during implementation these Arduino based shield are highly effected by temperature and results also changed due to high temperature.
Thesis