Keyword formal methods
-- No matches --

Model-based Synthesis of Generators for Embedded Systems

This research is sponsored by the DARPA MoBIES program. Its objective is to automate the creation of model interpreters and other, related tools used for semantic conversion of information.


Model-Integrated Computing for Surety of High Assurance Systems

Development formal-method based system design tools with an emphasis on reliability, safety, and security. The tools utilize models, generic in construct but domain specific for each application.


GME: The Generic Modeling Environment

GME is a configurable graphical modeling environment that supports building multi-aspect, hierarchical models. It also has flexible constraint management and automatic program synthesis capabilities.


Tools for formal modeling languages (4mlware)

Development of a formal backplane of tools that support analysis and interchange of models, metamodels, and DSMLs.


Kusy B., Abdelwahed S.: FTSP Protocol Verification using SPIN, ISIS-06-704, May, 2006.


Dubey A., Nordstrom S., Keskinpala T., Neema S., Bapty T.: Verifying Autonomic Fault Mitigation Strategies in Large Scale Real-Time Systems, Third IEEE International Workshop on Engineering of Autonomic & Autonomous Systems (EASE'06), pp. 129-140, Potsdam, Germany, March, 2006.


Dubey A., Xianbin Wu, Hang Su, Koo T.: Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach, Lecture Notes in Computer Science, 3707, pp. 114-128, October 11, 2005.


Dubey A.: Metamodel Based Language and Computation Platform for Algorithmic Analysis of Hybrid Systems, Master's Thesis, Vanderbilt University, Electrical Engineering, July 28, 2005.


Shetty S., Nordstrom S., Ahuja S., Yao D., Bapty T., Neema S.: Systems Integration of Autonomic Large Scale Systems Using Multiple Domain Specific Modeling Language, 12 IEEE International Conference Proceedings ECBS 2005, 12 IEEE International Conference on ECBS ,Engineering of Autonomic Systems, 0-7695-2306-0/05 pp481, Greenbelt, MD , USA, April 6, 2005.


Madl G., Abdelwahed S., Karsai G.: Automatic Verification of Component-Based Real-Time CORBA Applications, the 25th IEEE International Real-Time Systems Symposium, pp, Lisbon, Portugal, December, 2004.


Szemethy T., Karsai G.: Platform Modeling and Model Transformations for Analysis, Journal of Universal Computing Science, 10, 10, pp. 1383-1408, November 23, 2004.


Sprinkle J., Karsai G.: A Domain-Specific Visual Language For Domain Model Evolution , Journal of Visual Languages and Computing, vol. 15, no. 2, April, 2004.


Su R., Abdelwahed S., Karsai G., Biswas G.: Discrete Abstraction and Supervisory Control of Switching Systems, IEEE Int. Conference on Systems, Man & Cybernetics, (accepted), Washington, DC., October, 2003.


Sprinkle J.: Metamodel Driven Model Migration, Ph.D. Dissertation, Vanderbilt University, Electrical Engineering, August, 2003.


Abdelwahed S., Wonham W. M.: Blocking detection in discrete event systems, Proceeding of the American Control Conference, , Denver, CO, June, 2003.


Karsai G., Agrawal A., Shi F., Sprinkle J.: On the use of Graph Transformations in the Formal Specification of Computer-Based Systems, IEEE TC-ECBS and IFIP10.1 Joint Workshop on Formal Specifications of Computer-Based Systems, p. 19-27, Huntsville, Alabama, April 9, 2003.


Davis J.: Integrated Safety, Reliability, and Diagnostics of High Assurance, High Consequence Systems, Ph.D. Dissertation, Vanderbilt University, Electrical Engineering, May, 2000.


Davis J., Scott J., Sztipanovits J., Karsai G., Martinez M.: An Integtrated Multi-Domain Analysis Environment for High Consequence Systems, Proceedings of the 1998 ASME Design Engineering Technical Conference / Computers in Engineering, Paper No. 5532, Altanta, GA, September, 1998.


Davis J., Scott J., Sztipanovits J., Karsai G., Martinez M.: Integrated Analysis Environment for High Impact Systems, Proceedings of the Engineering of Computer Based Systems, pp. 218-225, Jerusalem, Israel, April, 1998.


Verification of complex finite-state systems

Finite-state systems with extremely large state-spaces often arise in common electro-mechanical systems. Yet, their formal verification is a difficult problem. In this effort we are developing techniques and tools based on symbolic model checking to perform these verification tasks.



Distributed Object Computing
Model-Integrated Computing
Model-Driven Architecture
Current Papers & Reports
Archived Papers & Reports