System design of a CC-NUMA multiprocessor architecture using formal specification, model-checking, co-simulation, and test generation

被引：19
作者：
Garavel H. [1 ]
Viho C. [2 ]
Zendri M. [3 ,4 ]
机构：
[1] INRIA Rhône-Alpes, 38330 Montbonnot St Martin
[2] IRISA/IFSIC Université de Rennes I, 35042 Rennes cedex, Campus de Beaulieu
[3] BULL R and D, 20010 Pregnana, Milanese, Via ai Laboratori Olivetti
[4] ST Microelectronics, 38240 Meylan
来源：
International Journal on Software Tools for Technology Transfer | 2001年 / 3卷 / 03期
关键词：
Cache coherency; cc-numa; Co-design; Co-simulation; Code generation; Computer architecture; Conformance testing; Formal methods; Formal specification; Hardware design; lotos; numa; Process algebra; Rapid prototyping; System level design; Test generation; Testing; Validation; Verification;
D O I：
10.1007/s100090100044
中图分类号：
学科分类号：
摘要：
The application of formal methods to the system-level design of hardware components is still an open issue for which concrete case-studies are needed. We present here an industrial experiment concerning the application of the process algebraic language lotos (iso standard 8807) to the design of polykid, a cc-numa (cache coherent - non-uniform memory access) multiprocessor architecture developed by bull. The formal descriptions developed for polykid have served as a basis not only for model-checking verification using cadp (caesar/aldebaran development package), but also for hardware-software co-simulation using the exec/caesartool, and for automatic generation of executable tests using the tgv tool. © 2001 Springer-Verlag.
引用
收藏
页码：314 / 331
页数：17
相关论文
共 47 条
  • [1] Bolognesi T., Brinksma E., Introduction to the ISO Specification Language LOTOS, Comput. Networks. ISDN Syst, 14, 1, pp. 25-59, (1988)
  • [2] Chehaibar G., Use of Formal Methods In POLYKID Development, (1997)
  • [3] Chehaibar G., Garavel H., Mounier L., Tawbi N., Zulian F., Specification and verification of the powerscale Bus Arbitration Protocol: An industrial experiment with LOTOS, Proc. Joint Int. Conf. On Formal Description Techniques For Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification FORTE/PSTV'96, Kaiserslautern, pp. 435-450
  • [4] Clarke E.M., Grumberg O., Hiraishi H., Jha S., Long D.E., McMillan K.L., Ness L.A., Verification of the futurebus+cache coherence protocol, Formal Methods Syst. Des, 6, 2, pp. 217-232, (1995)
  • [5] Composano R., Seawright A., Buck J., Modeling and Synthesis of Behavior, Control and Data Flow, Archit. Des. Validation Methods, pp. 1-48, (2000)
  • [6] de Meer J., Roth R., Vuong S., Introduction to Algebraic Specifications Based on the Language ACT ONE, Comput. Networks. ISDN Syst, 23, 5, pp. 363-392, (1992)
  • [7] Dubuis E., An Algorithm for Translating LOTOS Behavior Expressions into Automata and Ports, Proc. 2nd Int. Conf. On Formal Description Techniques FORTE'89, (1989)
  • [8] Ehrig H., Mahr B., Fundamentals of Algebraic Specification 1 Equations and Initial Semantics, EATCS Monographs On Theoretical Computer Science, 6, (1985)
  • [9] Eiriksson A.T., The Formal Design of 1M-gate ASICs, Formal Methods Syst. Des, 16, 1, pp. 7-22, (2000)
  • [10] Faci M., Logrippo L., Specifying Hardware in LOTOS, Int. Conf. On Computer Hardware Description Languages and Their Applications, pp. 305-312, (1993)
12345