5. Refleksjon rundt modellen
5.1. Den videreutviklede modellen
5.1.1. Sosio-demografiske egenskaper
É importante observar que a otimização aplicada aos refinamentos do método e ao código gerado é uma questão importante para o desenvolvimento smart card que ainda não foi tratada em profundidade no presente estudo. Conforme discutido no capítulo 8, nos trabalhos de Re- quet e Bossu [RB00], Bert [B+03] e Voisinet [Voi02], a geração de código otimizada para as
linguagens C e Java foi estudada no âmbito do projeto B with Optimized Memory (BOM), tendo em vista a instalação das aplicações desenvolvidas em smart cards.
Na continuação deste trabalho, deve-se pesquisar otimizações que possam ser inseridas diretamente sob forma de refinamento ao método BSmart, tais como a busca por padrões de refinamento de instruções e otimizações na declaração de variáveis de estado e na definição de variáveis locais. Observa-se que essas abordagens podem ser inicialmente descritas como um guia, e, nos casos onde for possível, inseridos em ferramenta. Nas situações em que não seja adequado introduzir em B, as otimizações serão acrescentadas durante a fase de tradução, utilizando-se as ideias dos trabalhos descritos anteriormente. Nesse sentido, identifica-se como otimização já aplicada ao tradutor, a criação de objetos persistentes dentro do método construtor da aplicação Java Card. Deve-se também buscar soluções para minimizar a criação de classes,
que atualmente são geradas a partir dos módulos de implementação (principal e módulos im- portados) e dos conjuntos adiados e enumerados.
9.3.4 KitSmart
Verificam-se diversas atividades que visam aprimorar o KitSmart, dentre elas, é possível destacar:
I. Revisar e, eventualmente, corrigir ou modificar os módulos B para tarefas que podem ser úteis ao desenvolvedor Java Card, tais como, internacionalização, manipulação de va- lores numéricos reais, etc. Devido a esses modelos originarem classes correspondentes em Java Card, deve-se refiná-los até o módulo de implementação e gerar a classe corres- pondente. Essas classes podem ser utilizadas em diferentes desenvolvimentos Java Card, contribuindo, portanto, para diminuir o retrabalho em verificação, tradução e compilação. A tarefa de geração de código deve ser feita com a ferramenta tradutora do BSmart, dessa forma tornando o desenvolvimento mais ágil e contribuindo para testar esse componente de software.
II. Pesquisar a melhor forma de se representar a tipagem com tipos abstratos de dados, le- vando em consideração a semântica de Java Card e o aspecto de verificação em B. Atual- mente, uma classe é representada sob a forma de um conjunto de mesmo nome da classe em Java. Uma subclasse em uma hierarquia de herança é tratada como um subconjunto do conjunto que representa a superclasse. Outra abordagem tentada foi modelar uma classe através de um struct em B, que corresponde a sua definição estática, e da instância de classe através de um record, representando o componente dinâmico, ou o objeto Java. As limitações dessa abordagem dizem respeito ao par struct/record lidar apenas com estado, sem permitir a definição de funções, e a falhas no provador do Atelier B tentar verificar corretamente as definições para uma estrutura. Uma primeira abordagem consiste em identificar a causa e solucionar esta falha, tendo em vista possibilitar o uso corretos das estruturas na representação de tipos.
III. Estudar toda a API Java Card para a versão Java Card 3.0 classic, evolução da API 2.2.2. Posteriormente, adaptar os módulos já desenvolvidos e criar novos modelos de acordo de modo a especificar a totalidade da API classic.
IV. Estudar a API Java Card 3.0 connected, verificando-se a viabilidade de fornecer a espe- cificação para essa versão da API, que possui uma gama maior de bibliotecas e recursos
encontrados na linguagem Java, tais como threads múltiplos, Strings, o tipo int, enum, genericse coleta de lixo.
V. Melhorar a abordagem para a especificação de exceções. Tendo em vista que o controle do lançamento de exceções é feito internamente pelo ambiente de execução (JCRE), inserir a modelagem do tratamento de situações de erro no modelo do JCRE e da sua interação com as aplicações componentes do ambiente Java Card. Outro aspecto a ser levado em consideração é o controle de transações, um tópico importante ao desenvolvimento Java Card, tendo em vista evitar que dados sob transação tornem-se inconsistentes após uma interrupção abrupta inesperada, como a retirada do cartão do leitor antes de um operação ser completada.
9.3.5 Estudo de Caso
O estudo de caso do passaporte eletrônico foi utilizado na validação do método, das biblio- tecas e ferramentas. Com esse propósito, especificou-se as máquinas e refinamentos necessários à implementação dos protocolos Basic Access Control (BAC) e Passive Authentication (PA), fundamentais para a autenticação e o acesso inicial aos arquivos de dados básicos do portador do documento armazenados no chip.
Como trabalho futuro espera-se desenvolver todos os recursos necessários requeridos pelos demais protocolos, a saber o Active Authentication (AA) e o Extended Access Control (EAC). Outro ponto a ser explorado diz respeito à especificação de parte da aplicação cliente. Nesse sentido, deve-se identificar quais componentes dessa aplicação podem ser inseridos, de modo a complementar a especificação e melhorar o aspecto de verificação global da aplicação. Com essa abordagem, torna-se possível refinar o cliente até a sua implementação B e gerar o código dessa parte da aplicação para Java.
Referências
[ABH+10] Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thai Son Hoang,
Farhad Mehta, and Laurent Voisin. Rodin: an open toolset for modelling and reasoning in Event-B. STTT, 12(6):447–466, 2010.
[Abr96] J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge Uni- versity Press, 1996.
[Abr10] J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cam- bridge University Press, 2010.
[B+03] Didier Bert et al. Adaptable translator of B specifications to embedded C pro-
grams. In FME, volume 2805 of LNCS, pages 94–113, September 2003.
[BBFM99] Patrick Behm, Paul Benoit, Alain Faivre, and Jean-Marc Meynadier. Météor: A Successful Application of B in a Large Project. In Formal Methods 99, volume 1708 of LNCS, 1999.
[BBK+07] Emilie Balland, Paul Brauner, Radu Kopetz, Pierre-Etienne Moreau, and An-
toine Reilles. Tom: piggybacking rewriting on Java. In Proceedings of the 18th international conference on Term rewriting and applications (RTA’07), pages 36–47, Berlin, 2007. Springer.
[BH94] J. P. Bowen and M. G. Hinchey. Seven more myths of formal methods: Dis- pelling industrial prejudices. In M. Naftalin, T. Denvir, and M. Bertran, editors, FME’94: Industrial Benefit of Formal Methods, pages 105–117. Springer, Ber- lin, 1994.
[BKV07] Mark Van Den Brand, Paul Klint, and Jurgen Vinju. The syntax definition formalism SDF, 2007. Available on: http://homepages.cwi.nl/˜daybuild/daily- books/syntax/sdf/sdf.html.
[BKV08] Mark Van Den Brand, Paul Klint, and Jurgen Vinju. The
language specification formalism ASF+SDF, 2008. Availa- ble on: http://homepages.cwi.nl/˜daybuild/daily-books/extraction- transformation/asfsdf/asfsdf.html.
[BP98] Richard Banach and M. Poppleton. Retrenchment: An engineering variation on refinement. In B’98: Proceedings of the Second International B Conference, pages 129–147, London, UK, 1998. Springer-Verlag.
[BR03] Lilian Burdy and Antoine Requet. Extending B with control flow breaks. In Proceedings of the 3rd international conference on Formal specification and development in Z and B, ZB’03, pages 513–527, Berlin, 2003. Springer.
[BY07] Michael Butler and Divakar Yadav. An Incremental Development of the Mondex System in Event-B. Formal Aspects of Computing, 20(1):61–77, 2007.
[CBR02] Ludovic Casset, Lilian Burdy, and Antoine Requet. Towards a full formal spe- cification of the Java Card API. In International Conference on Dependable Systems and Networks (DSN’02), pages 51–56. IEEE Computer Society, 2002. [CEF11] CEF. Página Web da Caixa Econômica Federal. Disponível em:
http://www.caixa.gov.br, 2011. Acesso em: 10 nov. 2011.
[Cer11] Certisign. Página Web do Certisign. Disponível em:
http://www.certisign.com.br/, 2011. Acesso em: 10 nov. 2011.
[Che00] Zhiqun Chen. Java Card Technology for Smart Cards: Architecture and Pro- grammer’s Guide. Addison Wesley, Boston, 2000.
[Cle12a] Clearsy. Atelier B tool. http://www.atelierb.eu/, 2012. Acesso em: 25 jun. 2012. [Cle12b] Clearsy. B-Compiler project. http://www.tools.clearsy.com/wp1/?page_id=153,
2012. Acesso em: 25 jun. 2012.
[Cle12c] Clearsy. ComenC tool. http://www.tools.clearsy.com/wp1/?page_id=59, 2012. Acesso em: 25 jun. 2012.
[Com10] Common Criteria. The Common Criteria Portal.
http://www.commoncriteriaportal.org/cc/, 2010.
[CW96] Edmund M. Clarke and Jeannette M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4):626–643, 1996.
[DGM06] David Déharbe, Bruno Gomes, and Anamaria Moreira. Automation of Java Card component development using the B method. In ICECCS, pages 259–268. IEEE Comp. Soc., 2006.
[DGM08] David Déharbe, Bruno Gomes, and Anamaria Moreira. BSmart: A Tool for the Development of Java Card Applications with the B Method. In ABZ, pages 351–352, 2008.
[dJ12] Ministério da Justiça. Registro de Identidade Civil. Disponível em: http://portal.mj.gov.br/ric, 2012. Acesso em: 5 jan. 2012.
[DLMP08] Frédéric Dadeau, Julien Lamboley, Thierry Moutet, and Marie-Laure Potet. A verifiable conformance relationship between smart card applets and B security models. In Proceedings of the 1st international conference on Abstract State Machines, B and Z (ABZ’08), pages 237–250, Berlin, 2008. Springer.
[dM12] Ernesto Brasil de Matos. Uma ferramenta para geração de testes de unidade a partir de especificações B. Mestrado, Programa de Pós-graduação em Sistemas e Computação, UFRN, Natal, 2012.
[DPT08] Frédéric Dadeau, Marie-Laure Potet, and Régis Tissot. A B formal framework for security developments in the domain of smart card applications. In IFIP 23rd International Information Security, pages 141–155, 2008.
[Dut06] Thiago Dutra. KitSmart: Um kit de tipos e estruturas de dados projetados com o método B para o desenvolvimento rigoroso em Java Card. Graduação, Depar- tamento de Informática e Matemática Aplicada, Universidade Federal do Rio Grande do Norte, Natal, 2006.
[EB10] Andy Edmunds and Michael Butler. Tool Support for Event-B Code Generation. Workshop On Tool Building in Formal Methods, ABZ 2010, Orford, CA, 2010. [Ecl10] Eclipse Foundation. Eclipse web site. www.eclipse.org. Last access: oct. 2010,
2010.
[Eur12] Eurosmart. Eurosmart expects over 7 billion smart secure devi- ces to be shipped in 2012. Technical report, Eurosmart, 2012. http://www.eurosmart.com/index.php/publications/market-overview.html. [FB07] Simon Fraser and Richard Banach. Configurable proof obligations in the Frog
toolkit. In Software Engineering and Formal Methods, pages 361–370, London, UK, 2007. IEEE Computer Society.
[FFW07] Leo Freitas, Zheng Fu, and Jim Woodcock. POSIX file store in Z/Eves: an experiment in the verified software repository. In Proceedings of the 12th IEEE International Conference on Engineering Complex Computer Systems, pages 3–14, Washington, DC, USA, 2007. IEEE Computer Society.
[FJM04] Houda Fekih, Leila Jemmi, and Stephan Merz. Transformation des spécificati- ons B en des diagrammes UML. In Proceedings of Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL’04), Besançon, June 2004. [Fra08] Simon Fraser. Mechanized Support for Retrenchment. PhD in computer sci- ence, Faculty of Engineering and Physical Sciences of University of Manches- ter, Manchester, UK, 2008.
[Gar06] Gary Leavens and Yoonsik Cheon. Design by Contract with JML. http://www.eecs.ucf.edu/˜leavens/JML/jmldbc.pdf, 2006.
[GDMM10] Bruno Gomes, David Déharbe, Anamaria Moreira, and Katia Moraes. Applying the B Method for the Rigorous Development of Smart card Applications. In Abstract State Machines, Alloy, B and Z (ABZ 2010), pages 203–216, Orford, Canada, 2010. Springer.
[Glo09] Global Platform. Global Platform Web site. Available on: http://www.globalplatform.org, 2009.
[GMD05] Bruno Gomes, Anamaria Moreira, and David Déharbe. Developing Java Card applications with B. In Brazilian Symposium on Formal Methods (SBMF), pages 63–77, 2005.
[GO09] Artur Gomes and Marcel Oliveira. Formal specification of a cardiac pacing system. In Proceedings of the 2nd World Congress on Formal Methods, FM’09, pages 692–707, Berlin, 2009. Springer.
[Gom07] Bruno Gomes. BSmart: Desenvolvimento Rigoroso de Aplicações Java Card com base no Método formal B. Master’s thesis, Universidade Federal do Rio Grande do Norte, Natal, 2007.
[Gom09] Bruno Gomes. Rigorous Development of Smart card Applications with the B method. In Proceedings of the Doctoral Symposium of Formal Methods 2009, pages 32–38, Eindhoven, The Netherlands, 2009. Technische Universi- teit Eindhoven.
[HMLS09] C. A. R. Hoare, Jayadev Misra, Gary T. Leavens, and Natarajan Shankar. The Verified Software Initiative: A manifesto. ACM Computing Surveys, 41(4), 2009.
[HNS+02] Uwe Hansmann, Martin Nicklous, Thomas Schäck, Achim Schneider, and
Frank Seliger. Smart Card Application Development Using Java. Springer, Berlim, 2002.
[HPP00] Wai-Ming Ho, Francois Pennaneac’h, and Noel Plouzeau. UMLAUT: A Fra- mework for Weaving UML-Based Aspect-Oriented Designs. In Proceedings of the Technology of Object-Oriented Languages and Systems (TOOLS 33), page 324, Washington, DC, USA, 2000. IEEE Computer Society.
[ICA06] ICAO. Machine Readable Travel Documents: Part I - Machine Readable Pass- ports. Technical report, International Civil Aviation Organization, 2006.
[ICA11] ICAO. Página Web da International Civil Aviation Organization. http://www2.icao.int/, 2011. Acesso em: 10 nov. 2011.
[IL04] A. Idani and Y. Ledru. Object Oriented Concepts Identifications from Formal B Specifications. In FMICS, September 2004.
[INR10] INRIA. The Coq Proof Assistant. http://coq.inria.fr/, 2010.
[ITI11] ITI. Página Web do Instituto Nacional de Tecnologia da Informação. Disponível em: http://www.iti.gov.br/twiki/bin/view/Main/WebHome, 2011. Acesso em: 10 nov. 2011.
[JJ05] Claude Jard and Thierry Jéron. TGV: theory, principles and algorithms: A tool for the automatic synthesis of conformance test cases for non-deterministic re- active systems. International Journal on Software Tools for Technology Transfer (STTT), 7(4):297–315, 2005.
[JUn10] JUnit.org. Junit: Resources for test driven development. http://www.junit.org/, 2010.
[KATP02] Pieter Koopman, Artem Alimarine, Jan Tretmans, and Rinus Plasmeijer. Gast: Generic Automated Software Testing. In 14th International Workshop on the Implementation of Functional Languages (IFL’02), number 2670 in LNCS, pa- ges 84–100, Madrid, Spain, 2002. Springer.
[Kli07] Paul Klint. Quick introduction to term rewriting, 2007. Available on: http://www.meta-environment.org/doc/books/extraction-transformation/term- rewriting/term-rewriting.html.
[KvdSV09] Paul Klint, Tijs van der Storm, and Jurgen Vinju. Rascal: A domain specific language for source code analysis and manipulation. Source Code Analysis and Manipulation, IEEE International Workshop on, 0:168–177, 2009.
[Lan00] Jean Louis Lanet. Are smart cards the ideal domain for applying formal methods? In ZB ’00: Proceedings of the First International Conference of B and Z Users on Formal Specification and Development in Z and B, pages 363–373, London, UK, 2000. Springer.
[Lar03] Daniel Larsson. OCL Specifications for the Java Card API. Master’s thesis, School of Computer Science and Engineering, Göteborg University, 2003. [LBBP10] Michael Leuschel, Michael Butler, Jeans Bendisposto, and Daniel
Plage. The ProB animator and model checker. http://www.stups.uni- duesseldorf.de/ProB/index.php5/Main_Page, 2010.
[LC06] Gary Leavens and Yoonsik Cheon. Design by contract with JML. Technical report, University of Central Florida, 2006.
[LM04] Daniel Larsson and Wojciech Mostowski. Specifying Java Card API in OCL. In Peter H. Schmitt, editor, OCL 2.0 Workshop at UML 2003, volume 102C of ENTCS, pages 3–19. Elsevier, November 2004.
[LS07] Thierry Lecomte and Thierry Servant. Formal methods in safety-critical railway systems. In 10th Brasilian Symposium on Formal Methods (SBMF2007), pages 1–, Ouro Preto, 2007.
[MC10] Georges Mariano and Samuel Colin. Brillant: an open source platform for B. Workshop on Tool Building in Formal Methods, ABZ 2010, Orford, CA, 2010. [MdB01] Hugues Martin and Lydie du Bousquet. Automatic test generation for Java-Card applets. In JavaCard ’00: Revised Papers from the First International Workshop on Java on Smart Cards: Programming and Security, pages 121–136, London, UK, 2001. Springer.
[MdMJD+08] Éberton Marinho, Valério de Medeiros Júnior, David Déharbe, Bruno Gomes,
and Cláudia Tavares. A Ferramenta Batcave para a Verificação de Especifica- ções Formais na Notação B. In XV Sessão de Ferramentas do XXII Simpósio Brasileiro de Engenharia de Software, pages 1–6, Campinas, 2008.
[ME09] Meta-Environment.org. The ASF+SDF Meta-Environment, 2009. Available on: http://www.meta-environment.org.
[MLF08] Hugo Daniel Macedo, Peter Gorm Larsen, and John S. Fitzgerald. Incremental development of a distributed real-time model of a cardiac pacing system using VDM. In Formal Methods 2008 (FM’08), pages 181–197, 2008.
[Mor07] Katia Moraes. Geração Automática de API’s para o Desenvolvimento de Apli- cações Cliente Java Card a partir da Especificação Formal. Graduação, Depar- tamento de Informática e Matemática Aplicada, Universidade Federal do Rio Grande do Norte, Natal, 2007.
[MP01] H. Meijer and E. Poll. Towards a Full Formal Specification of the Java Card API. In Smart Card Prog. and Security, volume 2140 of LNCS, pages 165–178. Springer, 2001.
[MP10] Wojciech Mostowski and Erik Poll. Electronic Passports in a Nutshell. Tech- nical Report ICIS–R10004, Radboud University Nijmegen, June 2010. Avai- lable at https://pms.cs.ru.nl/iris-diglib/src/getContent.php?id=2010-Mostowski- ElectronicNutshell.
[MT00] Stéphanie Motré and Corinne Téri. Using B Method to Formalize the Java Card Runtime Security Policy for a Common Criteria Evaluation. In 23rd National Information Systems Security Conference (NISSC 2000), pages 1–, 2000. [Mul10] MultOS. MultOS Web site. www.multos.com, 2010.
[Net07] Plácido Neto. Java card modelling language (JCML): Definição e Implemen- tação. Master’s thesis, Universidade Federal do Rio Grande do Norte, Natal, 2007.
[NPW10] Tobias Nipkow, Lawrence C. Paulson, and Markus Wen-
zel. Isabelle/HOL: A proof Assistant for High-Order Logic. http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf, 2010.
[OMG10] OMG. Object Constraint Language. http://www.omg.org/spec/OCL/, 2010. [OOS11] OOSTDIJK, M. et. al. JMRTD Project Web site. Disponível em:
http://jmrtd.org, 2011. Acesso em: 08 mar. 2011.
[Ora11] Oracle. Java card platform specification, version 2.2.2. http://java.sun.com/javacard/specs.html. Acesso em: jun. 2011, 2011.
[Ora12] Oracle. Java card 3.0 platform specification.
http://java.sun.com/javacard/3.0/specs.jsp. Acesso em: mar. 2012, 2012.
[Ort01] Ed Ort. Developing a Java Card Applet. Disponível em:
http://developers.sun.com/techtopics/mobility/javacard/articles/applet/, 2001. Acesso em: 1 dez. 2006.
[Ort03a] Enrique C. Ortiz. An Introduction to Java Card Technology. Available on: http://java.sun.com/javacard/reference/techart/javacard1, 2003.
[Ort03b] Enrique C. Ortiz. An Introduction to Java Card Technology. Disponível em: <http://developers.sun.com/techtopics/mobility/javacard/articles/javacard2>, 2003. Acesso em: 26 out. 2006.
[PC/09] PC/SC Workgroup. PC/SC Workgroup Web site. Available on: http://www.pcscworkgroup.com, 2009.
[Pol10] Polícia Federal. Passaporte Eletrônico.
http://www.dpf.gov.br/servicos/passaporte/passaporte-eletronico/, 2010. Acesso em: 15 fev. 2010.
[PvdBJ01] Erik Poll, Joachim van den Berg, and Bart Jacobs. Formal Specification of the Java Card API in JML: the APDU class. Computer Networks, 36(4):407–421, 2001.
[RB00] Antoine Requet and Gaëlle Bossu. Embedded formally proved code in a smart card: Converting B to C. In ICFEM’00, pages 15–, York, UK, 2000. IEEE Computer Society.
[RE03] Wolfgang Rankl and Wolfgang Effing. Smart Card Handbook. John Wiley, Baffins Lane, 3rd. edition, 2003.
[San12] Simone Santos. KitSmart: Uma biblioteca de componentes para o desenvolvi- mento rigoroso de aplicações Java Card com o método B. Mestrado, Programa de Pós-graduação em Sistemas e Computação, UFRN, Natal, 2012.
[SB06] Colin Snook and Michael Butler. UML-B: Formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol., 15(1):92–122, 2006.
[SB08] Colin Snook and Michael Butler. UML-B and Event-B: an integration of langua- ges and tools. In Proceedings of the IASTED International Conference on Soft- ware Engineering (SE’08), pages 336–341, Anaheim, CA, USA, 2008. ACTA Press.
[Sch01] Steve Schneider. The B-Method: An Introduction. Palgrave Macmillan, 2001. [SCW00] Susan Stepney, David Cooper, and Jim Woodcock. An electronic purse: Spe-
cification, refinement, and proof. Technical monograph PRG-126, Oxford Uni- versity Computing Laboratory, jul 2000.
[Ser07] Thierry Servant. Brama: A new graphic animation tool for B models. In B 2007: Formal Methods and Development in B, LNCS 4355, pages 274–276, Besançon, France, 2007. Springer.
[SL99] Denis Sabatier and Pierre Lartigue. The use of the B formal method for the design and the validation of the transaction mechanism for smart card applica- tions. In FM’99 - Formal Methods: World Congress on Formal Methods in the Development of Computing Systems, number 1708 in LNCS, pages 348–368, Toulose, France, 1999. Springer.
[SM10] Sun Microsystems. Java card platform specification 2.2.2. Disponível em: <http://java.sun.com/javacard/specs.html>, 2010. Acesso em: 03 ago. 2010. [Sou09] Fernanda Souza. Geração de casos de teste a partir de especificações B. Master’s
thesis, Universidade Federal do Rio Grande do Norte, Natal, 2009.
[Spi92] J.M. Spivey. The Z Notation: a Reference Manual. Prentice-Hall International Series in Computer Science. Prentice Hall, 2nd edition, 1992.
[Ter03] Terese. Term Rewriting Systems. Cambridge University Press, 1st edition, 2003. [THV02] B. Tatibouet, A. Hammad, and J. C. Voisinet. From Abstract B Specification to
[TRVH03] B. Tatibouet, A. Requet, J. C. Voisinet, and A. Hammad. Java Card Code Gene- ration from B Specifications. In ICFEM, volume 2885 of LNCS, pages 306–318, 2003.
[Vin05] Jurgen Vinju. Analysis and Transformation of Source Code by Parsing and Rewriting. PhD thesis, University of Amsterdam, 2005.
[Voi02] J. C. Voisinet. JBtools: an experimental platform for the formal B method. In Principles and Practice of Programming, pages 137–139, Maynooth, 2002. NUI.
[VSI10] VSI. The Verified Software Repository. http://vsr.sourceforge.net, 2010. [vWOF+05] Arjen van Weelden, Martijn Oostdijk, Lars Frantzen, Pieter W. M. Koopman,
and Jan Tretmans. On-the-fly formal testing of a smart card applet. In Security and Privacy in the Age of Ubiquitous Computing, IFIP TC11 20th International Conference on Information Security (SEC’05), pages 565–576, Chiba, Japan, 2005. Springer.