Name
Abstract | ||
|---|---|---|
In this paper we focus on design entry of complex systems, that is, the highest abstract tier of the global system without implementation choices to such and such technologies. At this very first level, the use of a formal specification language is more and more considered as the foundation of a real validation process. What we would like to emphasize is that from a formal design entry, project management can be formally controlled by formal refinement. We propose an architecture that is based upon stepwise refinement of a formal model to achieve controllable implementations. This leads to implementations that are highly effective, but remain formally related to the first formal specification. Partitioning, fault tolerance, and system management are seen as particular cases of refinement in order to conceptualize systems correct by proven construction. In this paper, we present the basic principles of system methodologies and describe the methodology based on the refinement paradigm. In order to prove this approach, we have developed the B-HDL Tool based on VHDL (digital circuits) and B method (formal language based on set theory and logic). The benefits of such tools would be an amazing productivity gain, a better reuse of automation and a formal redundancy management. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1109/DFTVS.2004.1347827 | DFT |
Keywords | Field | DocType |
productivity gain,automation reuse,stepwise refinement,formal redundancy management,formal design entry,formal mode stepwise refinement,refinement paradigm,b method,formal refinement,formal specification language,hardware description languages,complex system,system management,set theory,safety critical systems,co-design,logic partitioning,logic,fault tolerance,critical systems,project management,vhdl,hardware-software codesign,partitioning,redundancy,b-hdl tool,formal language,safety,validation process,formal specification,formal model,digital circuits,fault tolerant system | Formal equivalence checking,Formal language,Computer science,Real-time computing,Formal specification,B-Method,Refinement,Formal methods,Formal verification,Hardware description language | Conference |
ISSN | ISBN | Citations |
1550-5774 | 0-7695-2241-6 | 4 |
PageRank | References | Authors |
0.50 | 1 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ammar Aljer | 1 | 10 | 1.16 |
| Philippe Devienne | 2 | 131 | 19.93 |