In distributed systems and networks, such as the Air Traffic Management (ATM) system, peformance goals can only be reached if all actors cooperate. In Air Traffic Management (ATM), in order to satisfy future performance- and capacity-demands, increasingly sophisticated coordination procedures and resource allocation mechanisms are currently under development. These new mechanisms rely on extended data exchange as well as the communication of user-preferences and -constraints between actors and entirely new negotiation protocols. If the new mechanisms are designed properly, they ensure that Collaborative Decision Making (CDM) benefits can be realized and emergent system performance is indeed increased. However, the new mechanisms are, more than conventional centralized systems, more vulnerable to agents’ selfish, uncooperative behavior and manipulation. That kind of behavior can impair system performance. To make sure that CDM benefits can in fact be realized, system design has to take care that incentives established by the system are correctly aligned (i.e. compatible) with the design goals. The assumption of cooperative behavior becomes much more credible, if it can be proven that cooperative interaction with a given mechanism is actually in the best interest of each participating agent. The central contribution of this dissertation is the development of the framework DAVIC (Design and Verification of Incentive-Compatible Systems) which supports the modeling and realization of incentive-compatible systems. The framework is based on decision-theoretic, game-theoretic and system-theoretic analysis approaches as well as the net-based modeling of distributed agent systems with Coloured Petri Nets (CPN). Exploiting the CPN potential of a state space generation, extensive decision spaces are represented and agent- and system-reactions are explored. Through formal state space analysis, the explicit confrontation of overall system view and local agent view is realized. Based on the state space analysis techniques, DAVIC supports a systematic process of mechanism optimization and refinement. It enables the designer to select, based on decision-theoretic criteria and performance criteria, the optimal mechanism out of a pre-defined mechanism design space. The framework DAVIC consists of eight generic components whose functionality and interaction is explained in detail in this dissertation. The practical realization and implementation of the approach is demonstrated on the application example of an arrival planning mechanism from the domain of air traffic control.