Faculty Publications
Permanent URI for this communityhttps://idr.nitk.ac.in/handle/123456789/18736
Publications by NITK Faculty
Browse
4 results
Search Results
Item Arguing formally about flight control laws using SLDV and NUSMV(Springer Singapore, 2017) Jeppu, N.; Jeppu, Y.Software systems have failed in the recent past. This is most often attributed to wrong requirements often caught very late in the program or escapes from the rigorous process leading to failures. There is a necessity to ensure that the requirements are correct up front before the design and verification process start. Formal methods have become popular these days and a lot of impetus is there in the industry to apply these techniques to safety critical projects especially in flight controls. This paper looks at two tools NuSMV, an open source model checker, and Simulink Design Verifier, a commercial model checker. It is seen that these can be practically applied to projects and design. These are very successful in finding defects in design and requirements as demonstrated on a set of mutants. © Springer Nature Singapore Pte Ltd. 2018. All rights reserved.Item Teaching formal methods at undergraduate/graduate level: The three perspectives(Institute of Electrical and Electronics Engineers Inc., 2018) Jeppu, N.; Jeppu, Y.; Kavitha Devi, M.K.K.Formai methods provide easy way of validating properties about systems. These methods are in existence since the last 50 years but have not been used fully by the industry as an engineering tool. One of the challenges of acceptance is education. Educating engineering students to take up formal methods is a challenge. This paper looks at these aspects of formal methods by providing demonstration of its usefulness on a recent failure. A few challenges of teaching formal method are described and three perspectives of formal methods are explained. The viewpoints are from a student who has worked on this, a teacher who teaches this and an industry practitioner of formal methods. We advocate an industry academia partnership to overcome some of these challenges of teaching formal methods to students. © 2017 IEEE.Item Extending Denoising AutoEncoders for Feature Recognition(Institute of Electrical and Electronics Engineers Inc., 2018) Jeppu, N.; Chandrasekaran, K.Image rendering techniques involve the addition of noise on the rendered samples. The characteristics of Monte Carlo rendered noisy images makes it difficult to denoise using conventional methods. The noise induced in this case is spatially sparse. Using traditional methods of denoising and feature recognition is time consuming for such images as they use the entire image space as their search space. This results in unnecessary calculations that can be avoided and therefore reduce the processing time significantly. A recurrent convolutional neural network that operates on varying spatial resolutions, also known as the auto encoder decoder structure perform very well on these rendered images. The partitioning into encoder and decoder phases lets the network operate on continuously decreasing and increasing spatial domains respectively. This can be coupled with classification techniques to incorporate feature recognition of noisy images. In this paper the pretrained autoencoder layers are supported with additional softmax and sigmoid layers to enable feature recognition capabilities. © 2018 IEEE.Item CoCoA++: Delay gradient based congestion control for Internet of Things(Elsevier B.V., 2019) Rathod, V.; Jeppu, N.; Sastry, S.; Singala, S.; Tahiliani, M.P.In this paper, we propose a new congestion control algorithm called CoCoA++ to address the issue of network congestion in Internet of Things (IoT). Unlike the existing congestion control mechanisms that operate on instantaneous Round Trip Time (RTT) measurements in IoT, we use delay gradients to get a better measure of network congestion, and implement a probabilistic backoff to deal with congestion. We integrate the delay gradients and the probability backoff factor with Constrained Application Protocol (CoAP). The proposed algorithm is implemented and evaluated using the Cooja network simulator provided by Contiki OS. Subsequently, it is deployed and evaluated in a real testbed by using the FIT/IoT-LAB. We observe that delay gradients give a more accurate measure of congestion and the Retransmission Time Out (RTO) is reduced significantly, thereby leading to less delays and high packet sending rates. CoCoA++ being a minor improvement over the existing algorithm is easy to deploy. © 2019 Elsevier B.V.