Narrow Results

Encouraging informal firms to register with the government is a key policy issue for developing economies. However, the impact of formal registration on firm performance remains inconclusive. This paper constructs a nationally representative panel data set on registered and unregistered establishments in Cambodia by using the Economic Census in 2011 and the Inter-censal Economic Survey in 2014; the Economic Census surveyed all nonfarm establishments and enterprises without any establishment-size threshold, which served as a credible sample frame for the Inter-censal Economic Survey. To mitigate selection bias, I employ a difference-in-differences method combined with propensity-score matching and a propensity-score-weighted regression method. My results show that formalization has a significantly positive impact on sales, value added, and regularly employed workers, but yields little effect on labor productivity. While formal registration alone may not boost productivity, it can encourage the business growth of formalized firms by hiring more formal workers.

A use case is a specification of interactions involving a system and external actors of that system. The intuitive, user centered nature of textual use cases is one of the reasons for the success of the use case approach. A certain level of formalization is however needed to automate use case based system development, including tasks such as design synthesis, verification and validation. In this paper, a mapping from textual use cases to a formal model (Petri nets) is proposed. Use cases are described in a restricted-form of natural language. The abstract syntax of the language is formally defined using a tuple structure. The mapping from use cases to Petri nets considers use cases sequencing constraints defined at the syntactic-level, and provides a definition of execution semantics to use cases.

This paper proposes a novel strategy for formally analyzing functional requirements specification (FRS) and applies it to the Automatic Train Protection and Block (ATPB) system, which is proposed to reconstruct conventional rail lines in Japan. Based on the FRS in natural language, firstly, dynamic state transitions are extracted to express the operational mechanisms and determine the system parameters. A complete model of the ATPB system is then established using Unified Modeling Language (UML) to express the system structure graphically and explicitly. After achieving a common understanding, a VDM++ model is established formally to redescribe the original FRS of the ATPB system which is written in natural language (i.e. Japanese). Following that, in order to ensure internal consistency of the specification, proof obligations of the VDM++ model are discharged. Furthermore, a comprehensive testing is implemented to ensure that the FRS meets actual requirements. Finally, the system is simulated strictly in accordance with the formal specification. Without any runtime errors, collisions or derailments, the results of the simulation demonstrate the high quality and safety of the specification.

Software-Defined Networking (SDN) is an emerging architecture of computer networking. OpenFlow is considered as the first and currently most popular standard southbound interface of SDN. It is a communication protocol which enables the SDN controller to directly interact with the forwarding plane, which makes the network more flexible and programmable. The promising and widespread use makes the reliability of OpenFlow important. The OpenFlow bundle mechanism is a new mechanism proposed by OpenFlow protocol to guarantee the completeness and consistency of the messages transmitted between SDN devices like switches and controllers. In this paper, we use Communication Sequential Processes (CSP) to formally model the OpenFlow bundle mechanism. By adopting the models into the model checker Process Analysis Toolkit (PAT), we verify the relevant properties of the mechanism, including deadlock freeness, parallelism, atomicity, order property and schedulability. Our formalization and verification show that the mechanism can satisfy these properties, from which we can conclude that the mechanism offers a better way to guarantee the completeness and consistency.

Cyber-physical Systems (CPS) are widely used in all areas of life. Ensuring the correctness of CPS remains an enduring challenge during its development and design phases. One approach to ascertain the correctness of CPS is behavior equivalence based on bisimulation. However, whether the implementation development process develops in the right direction has an important impact on obtaining the correct system implementation. Especially, the development process of complex CPS often yields a multitude of implementation versions, the correlation among these versions partly signifies the correctness of the development process. This paper formalizes the relationship between the implementation versions and establishes a formal description of the development process progressing in the correct direction, leveraging the concept of a “limit idea.” Initially, we introduce the concept of “limit bisimulation” for CPS systems to delineate implementations acquired during the CPS development process. Specific limit bisimulations are demonstrated to represent distinct scenarios within the development process. Subsequently, the convergence mechanism of implementations is modeled through bisimulation limits, encapsulating the CPS’s specification as the ultimate goal of obtained implementations during the development process. Finally, the congruence property of the bisimulation limit is proved, which accounts for the relation between specification and implementation versions can be decomposed into a refinement hierarchy. The limit theorem of bisimulation in CPS can help the designer and developer of CPS to comprehend the development course better.

Nowadays medical software is tightly coupled with medical devices that perform patient state monitoring and lately even some basic treatment procedures. Medical guidelines (GLs) can be seen as specification of a medical system which requires their computer-interpretable representation of medical GLs. Until now most of the medical GLs are often represented in a textual format and therefore often suffer from such structural problems as incompleteness, inconsistencies, ambiguity and redundancy, which makes the translation process to the machine-interpretable language more complicated. Computer-based interpretation of GLs can improve the quality of protocols as well as the quality of medical service. Several GLs formal representation methods have been presented recently. Only some of them enable automatic formal verification by introducing an additional translation path to the existing model checking environments. However, if a verified property fails it is difficult to trace back the result needed to change the model. Moreover, these formalisms provide the notion of time mostly in terms of actions order. In this paper we preset the application of a well-know formal behaviour representation approach of embedded systems design domain to medical GLs interpretation. We use Timed Automata extended with Tasks (TAT) and TIMES toolbox to represent medical GLs as a system behaviour in a computer interpretable form. We discuss the verification issues with the help of the anticancer drug imatinib case study.

This paper presents a formal specification of the Assurance Point (AP) web service composition model. The AP model provides a flexible way of checking constraints and responding to execution errors in service composition. An AP is a combined logical and physical checkpoint, providing an execution milestone that stores critical data and interacts with integration rules (IRs) to alter program flow and to invoke different forms of recovery depending on the execution status. In this paper, the execution and recovery semantics of assurance points have been fully defined in the context of if-else, parallel, and loop control structures. The activities and complex control structures of the AP model have been formalized and tested in the Yet Another Workflow Language (YAWL) engine. By doing so, the correctness of the execution and recovery semantics in the AP model has been verified, demonstrating that YAWL nets of the AP model satisfy the soundness property. Different from existing web service composition models, the AP model presented by this research provides multiple levels of protection against service execution failure with a combination of forward and backward recovery techniques.

The rapidly growing informal micro and small-scale enterprise sector in Zimbabwe is an issue of concern because the government is still struggling to revive the economy from the effects of economic meltdown. Of main concern is the lost revenue through tax evasion. The growing informal sector is believed to be a result of the poor quality of certain institutions, high corruption levels in the country and lack of incentives to formalize. The objective of this study was to analyze the impact of growth constraints on the willingness to formalize by informal MSEs. Twenty internal and external growth inhibiting factors were analyzed using Principal Component Analysis (PCA) and a logistic model was estimated on a dichotomous variable of willing/not willing to formalize. The results show that willingness/unwillingness to formalize by informal entrepreneurs in Zimbabwe is significantly related to institutional imperfections and asymmetry of bureaucracy associated with the registration process, lack of access to technology, market and financial constraints and lack of entrepreneurial and management skills. Improving the bureaucracy of the registration process and access to technology may possibly increase the odds of the informal operators formalizing their businesses. However, improvement in market and financial constraints and entrepreneurial and managerial skills will decrease the odds of willingness to formalize.

Although research on entrepreneurship in the micro and small firms has been the subject of much scholarly attention, it has been mostly on the formal rather than informal economy. Drawing on the push and pull theory, this paper uses Principal Component Analysis to examine the motivations influencing entrepreneurs to venture into informal sector entrepreneurship in a specific South African municipal context. Against a background of addressing their constraints to growth, the prospects of formalization were considered, using logistic regression. The results, based on a sample of 160 entrepreneurs, show that even in the informal economy, pull factors are the uppermost motivations, apparently stronger than push factors, in influencing individuals to partake in microenterprise entrepreneurship. The logistic results indicate that even when some internal and external growth constraints are addressed, the likelihood of the entrepreneurs’ formalizing their business is not encouraging. Although alleviation of the growth hurdles may assist in enhancing entrepreneurial competence, it does not necessarily favor formalization, but enables a lock-in contentment effect to the informal sector. Against this inertia, implications for policy makers are presented.

Under what circumstances does firm formalization yield net benefits for previously informal firms? We systematically assessed 22 primary studies in a meta-analysis of African, Asian and Latin American firms. The studies are published between 2011 and 2021 and provide 1,372 performance and business practice estimates: 40 percent of the estimates show significantly positive and 54 percent insignificant effects. The FAT-PET analysis suggests a small positive effect of formalization on firm performance. We also employ a multivariate analysis: The overall genuine effect is modest. There is a positive role for information and time for effects to materialize. Notably, more rigorous designs and recent studies tend to identify smaller and more dispersed effects. The modest effects cast doubt about the capacity of formalization policies to improve business performances suggesting that policies might better focus on prioritizing business productivity and managerial capability over formalization. Yet, we need further experimenting and fine-tuning of policy approaches to precisely identify what could make the candle of formalization worth the effort. The current evidence supports theories arguing that the rational cost-benefit argument is an overly simplistic representation of the decision to formalize and that formalization is an uncertain decision affected by multiple and interrelated aspects.

Microenterprises have long been neglected in theoretical debates on the informal sector, receiving limited attention and superficial analysis. The aim of this article is to study the influence of the characteristics of informal microenterprises in Morocco on the decision to move to the formal sector. The article adopts a quantitative approach, focusing on 500 informal microentrepreneurs in northern Morocco. Through descriptive statistics and the use of a binomial logistic regression model, the study focuses on the effects of multiple aspects of these businesses. Data is collected and analyzed using the open-source tool R. The survey results reveal that engagement in a service-providing activity, the availability of business premises, and hiring more than four workers positively affect the propensity to formalize Moroccan informal microenterprises. Similarly, the use of simplified accounting systems, a longer period of existence and recourse to subcontracting are factors that encourage these ventures to opt for formalization. These findings are of key theoretical importance, exploiting the singularity of the Moroccan context and challenging the adoption of the neoliberal approach to explaining informality in Morocco. The conclusions are accompanied by recommendations designed to stimulate the transition to a formal sector. Implications of these findings for policy-makers, practitioners and entrepreneurs are discussed.

Small household businesses are widespread in Vietnam and are increasingly important for employment and economic growth. However, many are run informally which hinders their growth and harms the country’s economy as well. We utilize logistic regression based on the 2017 Economic Census and 2022 field survey data of formalized firms in Ho Chi Minh City. The size of the household business, use of information technology and revenue transparency influence the intention to convert household businesses into formal enterprises. The transition process can be complicated by various factors such as a household business owner’s unpreparedness, concerns about complications, fear of higher tax payments, limited internal resources, uncertain economic benefits and management regulations that are unsuitable for sole proprietorships.

Services form an important part of the economy today. Innovation for service firms is as important as for manufacturing, but the innovation process for service firms is comparatively little studied. In this paper, I review the literature there is on the innovation process for service firms, and make two suggestions for formalizing that process. The common thought that service firms do not innovate does not hold. Innovation is, however, often ad hoc for services, and it can therefore be difficult to measure firms' innovation efforts. These points are related to issues of appropriability of the benefits of innovation in services. The two issues primarily discussed in this paper — the possibilities of formalizing and appropriating in case of new service development — are central issues for service firms. It is here that this paper offers some contributions to the existing literature; it does not so much present an overview thereof.

In recent years, the front end of innovation has drawn a great deal of attention as an important driver of new product development (NPD) success. In this study, we analyze the impact of knowledge gathering, project planning, interfunctional collaboration and formalization on the ability to reduce technical and market uncertainties, creativity, and the efficiency of the early stages. 352 Austrian B2B-companies from technology-intensive sectors participated in the study. The results indicate that collaboration quality, formalization of the different phases of the front end and identification of customer-needs are fundamental for front-end performance, while collaboration quantity is less important. Moreover, planning was found to be central for efficiency and did not have a negative impact on creativity. Managerial recommendations from the study include scrutinizing the way in which interfunctional collaboration takes place, increasing customer integration and formalizing the early phases.

Do firms pay more taxes after formalization? The answer to this question is nontrivial. Tax noncompliance can be a persistent behavior among formerly informal firms. Analyzing the relationship between formalization and tax payments can also be challenging if nonswitching and switching firms have different characteristics. I use a panel dataset built from five small and medium-sized enterprise surveys conducted in Viet Nam from 2005 to 2013. By comparing nonswitching informal firms to switchers, I show that switchers are more likely to pay taxes and to pay a higher amount, thereby confirming heterogeneity. By comparing switchers before and after formalization, I find that formalization increases tax payment likelihood by 20% and the tax amount paid by 93%. A control function approach indicates that my results are robust to potential endogeneity of formalization. Therefore, this paper provides supportive evidence for a key public policy rationale to promote formalization: increased tax revenues.

The environment is the physical and social condition of human live, in which concepts play an important role in scientific discovery, technological innovation, social activities, and daily life. It is extremely important, therefore, to accurately describe the environment and a concept. This chapter aims to study environment formally, to trace the origin of a concept, and to govern the concept based on the formal environment in order to broaden the basis of the existing formal concept. To make the name of specific concept, the formal definition was briefly introduced.

Specification-based software development can allow the development, verification and maintenance of software at the specification level and can synthesis provably correct code. However, formal specification technology is hard to apply to the industrial development of software. UML has been used widely in the CASE-based software development. But, UML is a semiformal language and lacks formal semantics to express its meaning precisely. The paper proposes an approach for the formalization of UML statecharts mapped to RSL -a specification language based on coalgebra. The purpose is to bridge between UML and formal specification language.