Embedded systems often consist of deeply intertwined hardware and software components. At the same time, they are often used in safety-critical applications, where an error may result in enormous costs or even loss of human lives. Existing verification techniques that show the absence of errors do not scale well for complex integrated HW/SW systems. In this paper, we present a dependence analysis and automated partitioning approach for the formal analysis of HW/SW codesigns that are modeled in SystemC. The key idea of our approach is threefold: first, we partition a given system into loosely coupled submodels. Second, we analyze the dependences between these submodels and compute an abstract verification interface for each of them, which captures all possible influences of all other submodels. Third, we verify global properties of the overall system by verifying them separately for each subsystem. We demonstrate that our approach significantly reduces verification times and increases scalability with results for an anti-lock braking system.

Simulink is widely used in model-driven design.However, the complexity of hybrid systems that are modeled in Simulink limits the applicability of reuse techniques, which impedes cost-efficient design of complex systems. In particular, a systematic use and reuse of complex submodels, e.g. components with varying structure and functionality, is currently not supported. In this paper, we present an approach for service-oriented design in Simulink. The main idea is that we create a modular representation of complex Simulink structures as services with an expressive and formally defined dynamic interface. A dynamic interface captures not only the types of input and output signals but also their discrete and continuous behavior. Our main contribution is threefold: First, we introduce services in Simulink. Second, we transfer the concept of feature modeling to Simulink to express the variability of a service. Third, we introduce the novel concept of hybrid contracts to define the dynamic interface of a service. With our approach, we enable the designer (1) to define hybrid services that are reusable, and (2) to efficiently develop complex hybrid systems from a given set of services. We demonstrate this with a case study of a hybrid temperature control system.