| |
 |
|
|
|
Ramesh, S.
Indian Institute of Technology
Mumbai, India
|
|
|
 |
|
|
| |
| | S. Ramesh has been with with General Motors Global R&D for the last 10 years, where he currently holds the position of Technical Fellow and Thrust Area Lead for model-based embedded software. At General Motors, he is responsible for providing technical leadership for research and development in several areas related to electronics, control & software processes, methods, and tools. He has been an active industrial member of the Network for the Engineering of Complex Software-Intensive Systems for Automotive Systems (NECSIS), sponsored by the Automotive Partnership Canada. NECSIS is a research program focusing on making model-driven engineering into a mature industrial engineering methodology. As a member of NECSIS, Ramesh is responsible for monitoring and providing direction, and to facilitate interactions among the partners involved in NECSIS and GM Engineering. Earlier, Ramesh was on the faculty of the Department of Computer Science & Engineering at the Indian Institute of Technology Bombay (IITB), India, for more than 15 years. At IITB, he played a major role in setting up a National Centre for Formal Design and Verification of Embedded Software. His areas of research are rigorous software engineering, embedded systems, and real-time systems. He has published more than 100 papers in international journals and conferences. He has been on the editorial boards of the International Journal on Real-Time Systems and the Eurasip Journal on Embedded Systems and the IEEE Journal on Embedded System Letters. |
| |
| |
|
Date Reviewed |
|
| |
1 - 10 of 28
reviews
|
|
|
|
|
|
|
|
Modelling and verification of weighted spiking neural systems
Aman B., Ciobanu G. Theoretical Computer Science 623(C): 92-102, 2016. Type: Article
This paper considers the problem of formal verification of systems described using an abstract computing model called a spiking neural system, which is modeled after how brain cells (neurons) communicate. A spiking neural system is a c...
|
Jul 13 2016 |
|
|
|
|
|
|
Schedulability analysis of a graph-based task model for mixed-criticality systems
Ekberg P., Yi W. Real-Time Systems 52(1): 1-37, 2016. Type: Article
This paper is concerned with the problem of scheduling sporadic mixed-criticality tasks in uniprocessor systems. In these systems, tasks may not have fixed periods but minimum inter-arrival times. Further, they may have different criti...
|
Jul 13 2016 |
|
|
|
|
|
|
 Runtime verification of embedded real-time systems
Reinbacher T., Függer M., Brauer J. Formal Methods in System Design 44(3): 203-239, 2014. Type: Article
Runtime verification involves checking whether a given system (in software or hardware) satisfies a given property during the execution of the system. This paper presents a set of runtime verification algorithms, their correctness, and...
|
Aug 28 2015 |
|
|
|
|
|
|
Beginning Google Glass development
Tang J., Apress, Berkeley, CA, 2014. 368 pp. Type: Book (978-1-430267-88-1)
Google Glass embraces at least three technology areas (ubiquitous computing, Internet of Things, and wearable technologies), all of which find a place in any survey on recent technology trends. Like smartphones, Google Glass provides a...
|
Jan 6 2015 |
|
|
|
|
|
|
Modeling and analysis of TinyOS sensor node firmware: a CSP approach
McInnes A. ACM Transactions on Embedded Computing Systems 12(1): 1-23, 2013. Type: Article
This paper, as the name suggests, formalizes certain elements of TinyOS, an operating system that has become popular in the domain of sensor networks. The well-known formalism of communicating sequential processes (CSP) is used for mod...
|
Mar 8 2013 |
|
|
|
|
|
|
A logical verification methodology for service-oriented computing
Fantechi A., Gnesi S., Lapadula A., Mazzanti F., Pugliese R., Tiezzi F. ACM Transactions on Software Engineering and Methodology 21(3): 1-46, 2012. Type: Article
The focus of this paper is on formal modeling and analysis of service-oriented computing (Soc). The contributions of the paper are many: it proposes a specification language, SocL, for specifying service properties; it describes an abs...
|
Nov 8 2012 |
|
|
|
|
|
|
A parametric segmentation functor for fully automatic and scalable array content analysis
Cousot P., Cousot R., Logozzo F. ACM SIGPLAN Notices 46(1): 105-118, 2011. Type: Article
Precise and scalable static analysis of realistic software is challenging due to several complex features used in software. One of these features, which has been the focus of attention in recent times, is an array. In spite of several ...
|
Jun 1 2011 |
|
|
|
|
|
|
WYSINWYX: what you see is not what you execute
Balakrishnan G., Reps T. ACM Transactions on Programming Languages and Systems 32(6): 1-84, 2010. Type: Article
Source code analysis is a very well-known and well-developed area that deals with analyzing programs written in high-level languages to detect the presence of defects and to extract useful information about the program....
|
Nov 9 2010 |
|
|
|
|
|
|
Improving application security with data flow assertions
Yip A., Wang X., Zeldovich N., Kaashoek M. SOSP 2009 (Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, Big Sky, MT, Oct 11-14, 2009) 291-304, 2009. Type: Proceedings
Security violations and the unintended flow of important data are some of the problems faced by Web application developers. Yip et al. propose a methodology and a runtime system, RESIN, for avoiding and preventing such problems....
|
Jan 18 2010 |
|
|
|
|
|
|
Checking timed Büchi automata emptiness on simulation graphs
Tripakis S. ACM Transactions on Computational Logic 10(3): 1-19, 2009. Type: Article
This paper is broadly concerned with formal verification of timed systems. A well-known model of timed systems is the timed automaton, which is a class of finite state machine (FSM), equipped with one or more clocks for measuring the l...
|
Aug 7 2009 |
|
|
|
|
|
| |
|
|
| |
|
|
