Aplicação do método B ao projeto formal de software embarcado

This work shows a project method proposed to design and build software components from the software functional m del up to assembly code level in a rigorous fashion. This method is based on the B method, which was developed with support and interest of British Petroleum (BP). One goal of this methodology is to contribute to solve an important problem, known as The Verifying Compiler. Besides, this work describes a formal model of Z80 microcontroller and a real system of petroleum area. To achieve this goal, the formal model of Z80 was developed and documented, as it is one key component for the verification upto the assembly level. In order to improve the mentioned methodology, it was applied on a petroleum production test system, which is presented in this work. Part of this technique is performed manually. However, almost of these activities can be automated by a specific compiler. To build such compiler, the formal modelling of microcontroller and modelling of production test system should provide relevant knowledge and experiences to the design of a new compiler. In ummary, this work should improve the viability of one of the most stringent criteria for formal verification: speeding up the verification process, reducing design time and increasing the quality and reliability of the product of the final software. All these qualities are very important for systems that involve serious risks or in need of a high confidence, which is very common in the petroleum industry

Contribuições para verificação automática de applets javacard

The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification

Structural differentiation and corporate venturing : the moderating role of formal and informal integration mechanisms

Research has suggested that corporate venturing is crucial to strategic renewal and firm performance, yet scholars still debate the appropriate organizational configurations to facilitate the creation of new businesses in existing organizations. Our study investigates the effectiveness of combining structural differentiation with formal and informal organizational as well as top management team integration mechanisms in establishing an appropriate context for venturing activities. Our findings suggest that structural differentiation has a positive effect on corporate venturing. In addition, our study indicates that a shared vision has a positive effect on venturing in a structurally differentiated context. Socially integrated senior teams and cross-functional interfaces, however, are ineffective integration mechanisms for establishing linkages across differentiated units and for successfully pursuing corporate venturing.

Principals as architects of formal mentoring programs in schools

An important responsibility of principals in schools is fostering a healthy learning-rich environment for both staff and students. Previous research (Duignan & Gurr, 2008; Ehrich, 1998; Leithwood & Day, 2007; Nias, Southworth, & Campbell, 1992) has shown that effective principals create opportunities for teachers to learn with and from each other. For instance, they are involved in establishing supportive structures and creating environments for collaboration and learning to take place (Leithwood & Day, 2007). They do this in a variety of ways such as providing resources and professional development opportunities, structuring time for staff to learn and work together, and establishing a host of other conditions to facilitate learning and sharing.

The roles and importance of formal and informal sources of business support in young firms : evidence from the UK’s 2008 Federation of Small Business Survey

Objectives This research explores the relationship between young firms, their growth orientation-intention and a range of relationships which can be seen to provide business support. Prior-work Research indicates that networks impact the firm’s ability to secure resources (Sirmon and Hitt 2003; Liao and Welsch. 2004; Hanlon and Saunders 2007). Networks have been evaluated in a number of ways ranging from simple counts to characteristics of their composition (Davidsson and Honig 2003), strength of relationships (Granovetter 1973) and network diversity (Carter et al 2003). By providing access to resources and knowledge (from start-up assistance and raising capital, (e.g. Smallbone et al, 2003), networks may assist in enabling continued persistence during those times where firms may experience resource constraints owing to firm growth (Baker and Nelson 2005). Approach The data used in this research was generated in the 2008 UK Federation of Small Businesses (FSB) survey. Over 1,000 of the firms responding were found to fall into the category of “young”, ((defined as firms under 4 years old). Firms were considered the unit of analysis with the entrepreneur being the chief spokesperson for the firm. Preliminary data analysis considered key demographic characteristics and industry classifications, comparing the FSB data with that of the UK government’s own (BERR) Small Business Surveys of 2007 and 2008, to establish some degree of representativeness of the respondents. The analysis then examined networks with varying potential ability to provide support for young firms, the networks measured in terms of number, diversity, characteristic and strength in its relationship to young firm growth orientation. The diversity of business-support-related relationships ranged from friends and family, through professional services, customers and suppliers, and government business services, to trade associations and informal business networks. The characteristics of these formal and informal sources of support for new businesses are examined across a range of business support-type activities for new firms. The number of relationships and types of business support are also explored. Finally, the strength of these relationships is examined by analysis of the source of business support, type of business support, and links to the growth orientation-intention of the firm, after controlling for a number of key variables related to firm and industry status and owner characteristics. Results Preliminary analysis of the data by means of univariate analysis showed that average number of sources of advice was around 2.5 (from a potential total of 6). In terms of the diversity of relationships, universities had by far the smallest percentage of firms receiving beneficial advice from them. Government business services were beneficially used by 40% of young firms, the other relationship types being around the 50-55% mark. In terms of characteristics of the advice, the average number of areas in which benefit was achieved was around 5.5 of a maximum of 15. Start-up advice has by far the highest percentage of firms obtaining beneficial advice, with increasing sales, improving contacts and improving confidence being the other categories at or around the 50% mark. Other market-focused areas where benefits were also received were in the areas of new markets, existing product improvements and new product improvements, where around 40% of the young responding firms obtained benefit. Regression techniques evaluating the strength of these relationships in terms of the links between business support (by source of support, type of support, and range of support) and firm growth orientation-intention focus highlighted a number of significant relationships, even after controlling for a range of other explanatory variables identified in the literature. Specifically, there was found to be a positive relationship between receiving business advice generally (regardless of type or source) and growth orientation. This relationship was seen to be stronger, however, when looking at the number of types of beneficial advice received, and stronger again for the number of sources of this advice. In terms of individual sources of advice, customers and suppliers had the strongest relationship with growth, with Government business services also found to be significant. Combining these two sources was also seen to increase the strength of the relationship between these two sources of advice and growth orientation. In considering areas of support, growth was most strongly positively related to advice that benefited the development of new products and services, and also business confidence, but was negatively related to advice linked to business recovery. Finally, amalgamating the 4 key types and sources of advice to examine the impact of combinations of these types and sources of advice also improved the strength of the relationship. Implications The findings will assist in the understanding of young firms in general and growth more specifically, particularly the role and importance of specific sources, types and combinations of business support used more extensively by new young growth-oriented firms. Value This research may assist in processes designed to allow entrepreneurs to make better decisions; educators and support organizations to develop better advice and assistance, and Governments design better conditions for the creation of new growth-oriented businesses.

Attitudes to Formal Business Training and Learning amongst Entrepreneurs in the Cultural Industries: Situated Business Learning through "Doing with Others."

Presents arguments supporting a social model of learning linked to situated learning and cultural capital. Critiques training methods used in cultural industries (arts, publishing, broadcasting, design, fashion, restaurants). Uses case study evidence to demonstrates inadequacies of formal training in this sector. (Contains 49 references.)