Rigorous software design for nano and micro satellites using BIP framework
Graph Chatbot
Chat with Graph Search
Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.
DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.
UML State Machines constitute an integral part of software behavior specification within the Unified Modeling Language (UML). The development of realistic software applications often results in complex and distributed models. Hence, potential errors can be ...
Personal digital assistants or mobile phones applications are not anymore restricted to multimedia or wireless communications, but have been extended to handle Global Positioning System (GPS) functionalities. Consequently, the growing market of GPS capable ...
Turing Lecture from the winners of the 2007 ACM A.M. Turing Award.In 1981, Edmund M. Clarke and E. Allen Emerson, working in the USA, and Joseph Sifakis working independently in France, authored seminal papers that founded what has become the highly succes ...
A decade ago, Tony Hoare noted that "The real value of tests is not that they detect bugs in the code but that they detect inadequacies in the methods, concentration, and skills of those who design and produce the code." As usual, Tony saw far ahead of the ...
Modern software is reaching levels of complexity encountered in biological systems; sometimes comprising systems of systems each of which may include tens of millions of lines of code. Model Driven Engineering (MDE) advocates raising the level of abstracti ...
Symbolic execution has proven to be a practical technique for building automated test case generation and bug finding tools. Nevertheless, due to state explosion, these tools still struggle to achieve scalability. Given a program, one way to reduce the num ...
Symbolic execution has proven to be a practical technique for building automated test case generation and bug finding tools. Nevertheless, due to state explosion, these tools still struggle to achieve scalability. Given a program, one way to reduce the num ...
Personal Digital Assistants (PDAs) or mobile phones applications are not anymore restricted to multimedia or wireless communications, but have been extended to handle Global Navigation Satellite System (GNSS) functionalities. The new generation of portable ...
Inst Navigation, 815 15Th Th St Nw, Ste 832, Washington, Dc 20005 Usa2010
The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple ve ...
In contrast to beta-testing, formal verification can guarantee correctness of a program against a specification. Two basic verification techniques are theorem proving and model checking. Both have strengths and weaknesses. Theorem proving is powerful, but ...
