The verification of analog designs has been a challenging task for a few years now. Several approaches have been taken to tackle the main problem related to the complexity that such task presents to design and verification teams. The methodology presented in this document is based on the experiences and research work carried out by the Concordia University's Hardware Verification and the U. of Texas' IC systems design groups. The representation of complex systems where different interactions either mechanical or electrical take place requires an intricate set of mathematical descriptions which greatly vary according to the system under test. As a simple and very relevant example one can look at the integration of RF-MEMS as active elements in System-On-Chip architectures. In order to tackle such heterogeneous interaction for a consistent model, the use of stochastic hybrid models is described and implemented for very simple examples using high level modeling tools for a succinct and precise description. / text

No description available.

Abstraction-guided simulation is a promising semi-formal framework for design validation in which an abstract model of the design is used to guide a logic simulator towards a target property. However, key issues still need to be addressed before this framework can truly deliver on it's promise. Concretizing, or finding a real trace from an abstract trace, remains a hard problem. Abstract traces are often spurious, for which no corresponding real trace exits. This is a direct consequence of the abstraction being an over-approximation of the real design. Further, the way in which the abstract model is constructed is an open-ended problem which has a great impact on the performance of the simulator. In this work, we propose a novel approaches to address these issues. First, we present a genetic algorithm to select sets of state variables directly from the gate-level net-list of the design, which are highly correlated to the target property. The sets of selected variables are used to build the Partition Navigation Tracks (PNTs). PNTs capture the behavior of expanded portions of the state space as they related to the target property. Moreover, the computation and storage costs of the PNTs is small, making them scale well to large designs. Our experiments show that we are able to reach many more hard-to-reach states using our proposed techniques, compared to state-of-the-art methods. Next, we propose a novel abstraction strengthening technique, where the abstract design is constrained to make it more closely resemble the concrete design. Abstraction strengthening greatly reduces the need to refine the abstract model for hard to reach properties. To achieve this, we efficiently identify sequentially unreachable partial sates in the concrete design via intelligent partitioning, resolution and cube enlargement. Then, these partial states are added as constraints in the abstract model. Our experiments show that the cost to compute these constraints is low and the abstract traces obtained from the strengthened abstract model are far easier to concretize. / Master of Science

This research investigates the role business incubators on the MSMEs’ access to informal and semi-formal finance. To meet this purpose, firstly, the relationship between business incubation models and models of financial accessibility is assessed. secondly, the contribution of business incubators to the MSMEs informal and semi-formal financial accessibility is determined, by assessing the direct impact of monitoring services on financial accessibility and also assessing the incubator’s financial intermediation role between incubatees and financiers. Due to the important role played by social capital in non-formal financing, the influence of both incubatee and incubator manager’s social capital on incubatee’s informal and semi-formal financial accessibility is also investigated. The results indicate that, business incubator’s monitoring services have significant positive influence on incubatee’s access to informal and semi-formal finance, and also there is a significant positive relationship between monitoring services and financial management capabilities. Also, incubatee’s financial management capabilities have significant positive impact on semi-formal financial accessibility, nevertheless, there is insignificant relationship between incubatee’s financial management capabilities and informal financial accessibility. Furthermore, the results show, incubatee’s bonding and bridging social capital have direct positive impact on both informal and semi-formal financial accessibility, while incubator manager’s linking social capital has positive impact on semi-formal financial accessibility but insignificant impact on informal financial accessibility. Incubatee’s bridging social capital also negatively moderates the relationship between financial management capabilities and semi-formal financial accessibility, whereas incubatee’s bonding has no moderating effect on the same relationship. Incubator manager’s bonding and bridging social capital and incubatee’s linking social capital have insignificant direct impact on both informal and semi-formal financial accessibility, as well as insignificant moderating impact on the relationship between financial management capabilities and semi-formal financial accessibility. These findings show the importance of financial management capabilities on incubatee’s access to semi-formal finance and highlights the role of incubatee’s bonding and bridging network links and incubator manager’s linking social networks to the incubatee’s access to non-formal finance. They also reveal that informal financiers do not consider incubatee’s financial management capabilities as an important criterion in deciding to provide them credits:Acknowledgement i Table of contents iii List of tables viii List of figures xii Abbreviations xv Zusammenfassung xx Summary xxxii CHAPTER ONE 1 INTRODUCTION 1 1.1 Background to the problem 1 1.2 Statement of the Problem 4 1.3 Objectives of the study 10 1.3.1 General objective 10 1.3.2 Specific objectives 10 CHAPTER TWO 11 LITERATURE REVIEW 11 2.1 Start-ups and Micro, Small and Medium Enterprises 11 2.1.1 Micro, Small and Medium Enterprises 11 2.1.1.1 MSMEs’ sector in Tanzania 14 2.1.2 Start-ups 15 2.1.2.1 Startups in Tanzania 16 2.2 Business incubators 18 2.2.1 Services provided by business incubators 21 2.2.2 Business incubators in Tanzania 23 2.3 Financial management capabilities 28 2.3.1 Financial management capabilities in MSMEs 29 2.4 Financial system 32 2.4.1 Formal financing 33 2.4.2 Informal financing 33 2.4.3 Semi-formal financing 34 2.4.4 Financing system in Tanzania 34 2.4.5 Informal and Semi-formal financing system in Tanzania 36 2.4.5.1 Informal financiers 37 2.4.5.2 Semi-formal financiers 45 2.5 MSMEs’ financial accessibility 52 2.5.1 MSMEs’ financial accessibility in Tanzania 55 2.5.2 The role of business incubators in promoting MSMEs’ access to finance 56 2.6 Information asymmetries between MSMEs and financiers 59 2.7 Theory of financial intermediation 61 2.8 Social capital 62 2.8.1 Role of social capital on MSMEs’ access to finance 65 2.9 Summary of the theoretical framework 69 2.10 Proposed model 70 CHAPTER THREE 75 RESEARCH METHODOLOGY 75 3.1 Research Design 75 3.2 Study Area 76 3.3 Targeted population 78 3.4 Sample 79 3.5 Operational definitions and measurement of the variables 83 3.5.1 Variable indicators 83 3.5.2 Business incubators' monitoring services 83 3.5.3 Financial management capabilities 84 3.5.4 Incubatee's bonding social capital 84 3.5.5 Incubatee's bridging social capital 85 3.5.6 Incubatee's linking social capital 85 3.5.7 Incubator manager's bonding social capital 86 3.5.8 Incubator manager's bridging social capital 86 3.5.9 Incubator manager's linking social capital 87 3.5.10 MSMEs’ Financial accessibility 87 3.6 Data collection instrument 92 3.6.1 Questionnaire 92 3.6.2 Personal interviews 93 3.7 Data collection 93 3.8 Data Analysis 94 3.8.1 Qualitative data analysis 94 3.8.2 Quantitative analysis 95 3.8.2.1 Data preparation 95 3.8.2.2 Descriptive statistics 96 3.8.2.3 Factor analysis 96 3.8.2.4 Inferential Statistics 104 3.8.2.4.1 Spearman correlations analysis 105 3.8.2.4.2 Kruskal-Wallis test 105 3.8.2.4.3 Partial Least Squares regressions analysis 105 3.9 Validity and Reliability 106 3.9.1 Validity and reliability of qualitative research 106 3.9.2 Validity and reliability in quantitative research 107 CHAPTER FOUR 110 PRESENTATION OF FINDINGS 110 4.1 Introduction 110 4.2 Qualitative results 110 4.2.1 Current status of business incubation programs in Tanzania 110 4.2.2 Factors for business incubators’ successful financial intermediary role118 4.3 Quantitative results 132 4.3.1 Descriptive results 132 4.3.1.1 Sample demography 133 4.3.1.1.1 Relationship between age and incubation period of incubated MSMEs 133 4.3.1.1.2 Categorizing incubated MSMEs by number of employees and business capital 135 4.3.1.1.3 Distribution of incubatees by their nature of ownership and business activity 138 4.3.1.1.4 Financiers’ provision of requested amount of loans to incubatees 140 4.3.1.2 The contribution of business incubators to MSMEs financial accessibility 145 4.3.1.2.1 The Business Incubator's Monitoring services 146 4.3.1.2.2 Financial Management capabilities of incubatees 147 4.3.1.2.3 MSMEs’ financial accessibility 149 4.3.1.3 Relationship between business incubation models and models of MSMEs financing 150 4.3.1.4 Factors for successful intermediary role of an incubator 152 4.3.1.5 Incubatees and incubator managers’ social capital on Incubatees' financial accessibility 155 4.3.2 The impact of business incubation on MSMEs access to informal and semi-formal finance 160 4.3.2.1 Demographic characteristics of incubated enterprises 161 4.3.2.2 Relationship between business incubation models and models of financial accessibility 165 4.3.2.3 Contribution of incubators to the MSMEs informal and semi-formal financial accessibility 166 4.3.2.3.1 Impact of business incubator’s monitoring services on MSMEs’ informal and semi-formal financial accessibility 167 4.3.2.3.2 Business incubators’ financial intermediation role between incubated MSMEs and financiers. 170 4.3.2.4 Impact of incubatee and incubator manager’s social capital on iMFA and sMFA 173 4.3.2.5 Moderating impact of Incubatee's and incubator manager's social capital on the FMC-MFA relationship 179 4.4 Summary of chapter four 183 4.4.1 Developing a model on incubated MSMEs’ access to informal and semi- formal finance. 190 4.4.1.1 A model on incubated MSMEs’ access to informal finance 190 4.4.1.2 A model on incubated MSMEs’ access to semi-formal finance. 191 4.4.1.3 The influence of demographic characters on the relationship between social capital and financial accessibility. 192 CHAPTER FIVE 196 DISCUSSION OF FINDINGS 196 5.1 Introduction 196 5.2 Demographic characteristics of incubatees 196 5.3 Relationship between business incubation models and models of financial accessibility 201 5.4 Business incubators’ financial intermediation role between MSMEs and financiers. 203 5.5 Factors for successful business incubator’s financial intermediary role 207 5.6 Impact of incubatee’s and incubator manager’s social capital on informal and semi-formal financial accessibility 209 5.7 Moderating impact of Incubatee's and incubator manager's social capital on the FMC-MFA relationship 212 CHAPTER SIX 214 CONCLUSIONS AND RECOMMENDATIONS 214 6.1 Conclusions 214 6.2 Recommendations 221 6.3 Scope for further research 229 Reference 234 Appendix I Total Variance Explained 253 Appendix II Component Matrix 254 Appendix III Pattern Matrix 255 Appendix IV Questionnaire 256 Appendix V Questionnaire (Swahili version) 261 Appendix VI Interview guide for the financiers (English version) 266 Appendix VII Interview guide for the financiers (Swahili version) 267 Apendix VIII Interview guide for incubators’ managers and key informants (English version) 268 Appendix IX Interview guide for incubators’ managers and key informants (Swahili version) 269 Appendix X Eigenständigkeitserklärung 270

Formal specification of software systems has been very promising. Critics against the end results of formal methods, that is, producing quality software products, is certainly rare. Instead, reasons have been formulated to justify why the adoption of the technique in industry remains limited. Some of the reasons are: • Steap learning curve; formal techniques are said to be hard to use. • Lack of a step-by-step construction mechanism and poor guidance. • Difficulty to integrate the technique into the existing software processes. Z is, arguably, one of the successful formal specification techniques that was extended to Object-Z to accommodate object-orientation. The Z notation is based on first-order logic and a strongly typed fragment of Zermelo-Fraenkel set theory. Some attempts have been made to couple Z with semi-formal notations such as UML. However, the case of coupling Object-Z (and also Z) and the Use Case Maps (UCMs) notation is still to be explored. A Use Case Map (UCM) is a scenario-based visual notation facilitating the requirements definition of complex systems. A UCM may be generated either from a set of informal requirements, or from use cases normally expressed in natural language. UCMs have the potential to bring more clarity into the functional description of a system. It may furthermore eliminate possible errors in the user requirements. But UCMs are not suitable to reason formally about system behaviour. In this dissertation, we aim to demonstrate that a UCM can be transformed into Z and Object-Z, by providing a transformation framework. Through a case study, the impact of using UCM as an intermediate step in the process of producing a Z and Object-Z specification is explored. The aim is to improve on the constructivity of Z and Object-Z, provide more guidance, and address the issue of integrating them into the existing Software Requirements engineering process. / Computer Science / M. Sc. (Computer Science)

Formal specification of software systems has been very promising. Critics against the end results of formal methods, that is, producing quality software products, is certainly rare. Instead, reasons have been formulated to justify why the adoption of the technique in industry remains limited. Some of the reasons are: • Steap learning curve; formal techniques are said to be hard to use. • Lack of a step-by-step construction mechanism and poor guidance. • Difficulty to integrate the technique into the existing software processes. Z is, arguably, one of the successful formal specification techniques that was extended to Object-Z to accommodate object-orientation. The Z notation is based on first-order logic and a strongly typed fragment of Zermelo-Fraenkel set theory. Some attempts have been made to couple Z with semi-formal notations such as UML. However, the case of coupling Object-Z (and also Z) and the Use Case Maps (UCMs) notation is still to be explored. A Use Case Map (UCM) is a scenario-based visual notation facilitating the requirements definition of complex systems. A UCM may be generated either from a set of informal requirements, or from use cases normally expressed in natural language. UCMs have the potential to bring more clarity into the functional description of a system. It may furthermore eliminate possible errors in the user requirements. But UCMs are not suitable to reason formally about system behaviour. In this dissertation, we aim to demonstrate that a UCM can be transformed into Z and Object-Z, by providing a transformation framework. Through a case study, the impact of using UCM as an intermediate step in the process of producing a Z and Object-Z specification is explored. The aim is to improve on the constructivity of Z and Object-Z, provide more guidance, and address the issue of integrating them into the existing Software Requirements engineering process. / Computer Science / M. Sc. (Computer Science) / D. Phil. (Computer Science)

The growing need for computer software in different sectors of activity, (health, agriculture, industries, education, aeronautic, science and telecommunication) together with the increasing reliance of the society as a whole on information technology, is placing a heavy and fast growing demand on complex and high quality software systems. In this regard, the anticipation has been on non-functional requirements (NFRs) engineering and formal methods. Despite their common objective, these techniques have in most cases evolved separately. NFRs engineering proceeds firstly, by deriving measures to evaluate the quality of the constructed software (product-oriented approach), and secondarily by improving the engineering process (process-oriented approach). With the ability to combine the analysis of both functional and non-functional requirements, Goal-Oriented Requirements Engineering (GORE) approaches have become de facto leading requirements engineering methods. They propose through refinement/operationalisation, means to satisfy NFRs encoded in softgoals at an early phase of software development. On the other side, formal methods have kept, so far, their promise to eliminate errors in software artefacts to produce high quality software products and are therefore particularly solicited for safety and mission critical systems for which a single error may cause great loss including human life. This thesis introduces the concept of Complementary Non-functional action (CNF-action) to extend the analysis and development of NFRs beyond the traditional goals/softgoals analysis, based on refinement/operationalisation, and to propagate the influence of NFRs to other software construction phases. Mechanisms are also developed to integrate the formal technique Z/Object-Z into the standardised User Requirements Notation (URN) to formalise GRL models describing functional and non-functional requirements, to propagate CNF-actions of the formalised NFRs to UCMs maps, to facilitate URN construction process and the quality of URN models. / School of Computing / D. Phil (Computer Science)